HomeIsabelle/Phabricator

merge from afp-2020

Authored by kleing.

Description

merge from afp-2020

Merged Changes

This commit merges a very large number of changes. Only the first 50 are shown.
CommitAuthorDetailsCommitted
aade54113506Sophie Tourret
saturation framework: completes standard_lifting restructuration 
Sep 7
21bc345f5a27florian.haftmann
generalized signed_take_bit 
Sep 5
3c01c6d69e78florian.haftmann
more on conversions 
Sep 5
d99a51136b97Sophie Tourret
saturation framework: fills standard lifting locale 
Sep 4
0a2b5e06621cblanchette
renamings 
Sep 3
075c0450120dblanchette
tuned notation 
Sep 2
f15cc3b9e238paulson
a repair and considerable reformatting 
Sep 2
a22073e6cb92blanchette
tuning 
Sep 1
cb48e644eda2makarius
adapted to "subst" of Isabelle/e5fcbf6dc687; 
Aug 31
59b5d2617e31makarius
more systematic support for special directories (see Isabelle/5894859c5c84); 
Aug 31
516d4e0ad2e0Sophie Tourret
fix latex compilation of saturation framework 
Aug 31
f87125c95a68paulson
removal of library theorems that were already in Isabelle main 
Aug 31
91ce4a639768Sophie Tourret
comments in saturation framework 
Aug 31
f22a73cc49a1blanchette
tuned arrows, and proofs 
Aug 31
c812b6895caapaulson
variable renaming 
Aug 30
023af1e22f70florian.haftmann
more on conversions 
Aug 30
656918360168paulson
merged 
Aug 28
9c86034d4adfpaulson
the last quantifier tweaks 
Aug 28
bfee570e953eblanchette
mild renamings in saturation framework 
Aug 28
ef75bcbbe619paulson
merged 
Aug 28
aa61d7d2a5fcpaulson
quantifier fixes 
Aug 28
9f61d06c57fcblanchette
simplified 'length = 0' 
Aug 28
f42d5b45465dWalter Guttmann
adapted uses of vcg_tc_simp in Aggregation_Algebras and… 
Aug 27
c1979202233dblanchette
tuned document 
Aug 26
e4e449d5b763blanchette
merged two theory files and cleaned up some locales 
Aug 26
5a968d3e072bRene Thiemann
fixes for Relational_Disjoint_Set_Forests (AFP 2020 -> devel) 
Aug 26
a51281787c8bRene Thiemann
merge of AFP 2020, fixed some proofs, but Relational_Disjoint_Set_Forests stays… 
Aug 26
821ca76f3c0dpaulson
sitegen for Saturation_Framework_Extensions (and also for five other entries) 
Aug 25
ac00f34583b0paulson
new entry Saturation_Framework_Extensions 
Aug 25
a41d53bc4c69florian.haftmann
a proof of concept for generic conversions 
Aug 24
a7b99e8a1d84florian.haftmann
tuned 
Aug 22
d4c56b2760cfpaulson
reversing all the lex crap 
Aug 21
c47e491d6c30paulson
merged 
Aug 20
242c8f6d0acepaulson
more lex fixes, some tricky 
Aug 20
7d42634829a4blanchette
removed double underscores + tuned comments 
Aug 20
52090471320fblanchette
bring title of document in sync with title of entry 
Aug 20
d2a0a7ac2b78paulson
fixing some lex problems 
Aug 19
62b7aa536380paulson
more lex fixes 
Aug 19
fcf802f31002paulson
some lex fixes 
Aug 18
05908e2bd514paulson
fixes for new-style definition of lexicographic ordering 
Aug 18
a067d7a7ff67makarius
clarified signature (see Isabelle/2b41b710f6ef); 
Aug 14
d31906039242Joshua Schneider
reduced redundancy by sharing theories with MFOTL_Monitor; 
Aug 14
3c4396a19260Joshua Schneider
MFOTL_Monitor change history 
Aug 13
b1639ed541b7Joshua Schneider
added abstract slicing framework to MFOTL_Monitor; 
Aug 13
9a9bc053eb71florian.haftmann
dedicated symbols for code generation, to pave way for generic conversions from… 
Aug 10
7950cea20592paulson
merged 
Aug 9
633328cc6a47paulson
more on order types 
Aug 9
116a82414c28florian.haftmann
dropped alias 
Aug 6
3e79743d7844florian.haftmann
separation of reversed bit lists from other material 
Aug 5
cac1c67360f3florian.haftmann
further refinement of code equations for mask operation 
Aug 5