HomeIsabelle/Phabricator

merge from afp-2020

Authored by kleing.

Description

merge from afp-2020

Details

Committed
kleingSun, May 17, 8:27 AM
Parents
rAFP9a777766b777: New entry: Knuth_Bendix_Order
rAFP3f26cf4e20e8: admin/sitegen (with python3)
Branches
Unknown
Tags
Unknown

Merged Changes

This commit merges a very large number of changes. Only the first 50 are shown.
CommitAuthorDetailsCommitted
3f26cf4e20e8Christian Sternagel
admin/sitegen (with python3) 
May 15
e6ecfda4c915Christian Sternagel
added email address 
May 15
bca5d31690deblanchette
moved theory files from IsaFoL repository to AFP now that IsaFoR's KBO is in… 
May 15
cd4388702c9bnipkow
New entry Knuth_Bendix_Order 
May 15
2fb9e44335afblanchette
merge 
May 15
1e1d92130953blanchette
added two lemmas 
May 15
80a61392b4aaJulian Brunner
merged 
May 15
2a8c0c859b0aJulian Brunner
refactoring 
May 15
018736453df4Julian Brunner
refactoring 
Apr 27
231c5cb952edpruvisto
adapted to isabelle-dev/07c85c68ff03 
May 15
a3c410f7ad14blanchette
merge 
May 15
afa6f540c178blanchette
added lemma about limits 
May 15
4acc6a5c1603nipkow
adapted to f4626b1f1b96 
May 15
6c077dc51be0blanchette
various extensions and simplifications to the theorem proving libraries 
May 15
3483f9d26850blanchette
added lemmas 
May 14
68699ec0d47eblanchette
tuning 
May 14
f4451bba95a2blanchette
simplified proof 
May 14
24488f2cadddpruvisto
adapted to isabelle-dev/c095d3143047 
May 13
b5739aa85c75blanchette
uniformize capitalization 
May 13
f01859e37d6bblanchette
added lemmas 
May 13
a0d27ac848aapaulson
Max/Sup issue 
May 12
60ace64e5efapaulson
merged 
May 12
0bfe1a85f42apaulson
corrections for Sup{} = (0::nat) 
May 12
9c544f77d299nipkow
final lower case of topics 
May 12
55c932d460f7blanchette
about to give up 
May 12
8274c4ccd8c9blanchette
moved lemmas around, tuning 
May 12
3a7847bc58ceblanchette
moving lemmas where they belong 
May 11
9fdbd41ffa9anipkow
lower case topics following AMS and ACM 
May 11
ee34afb2b57cblanchette
added lemmas 
May 11
035769df3336blanchette
generalized completeness theorems + refactored a little 
May 11
77ad5390bcd8blanchette
added lemmas 
May 11
a7dec07bb044blanchette
added two lemmas 
May 11
818b453ae7cbpaulson
removal of legacy binding 
May 11
2e7ac4fd9a3fblanchette
simplified proof 
May 11
982c9eb51fe6blanchette
rationalized locales 
May 11
4c337328e727blanchette
removed abbreviation that only lengthened formalization 
May 11
ff58aa530358blanchette
rationalized locales 
May 11
f67a3c3fcc17blanchette
rationalized locales 
May 11
bb1e74987268blanchette
rationalized locales 
May 11
5058f17437d6blanchette
rationalized locales 
May 11
c9078e5ff173blanchette
simplified locale setup + replaced some definitions by abbreviations 
May 10
fd511536d43dblanchette
rationalized locales 
May 9
5ded9bf522f3blanchette
rationalized locales, reducing aliasing 
May 9
e3d9183d726aflorian.haftmann
modernized notation for bit operations 
May 9
08aac5b9f7c0blanchette
removed prefixes on key sublocales 
May 8
a9a2c8a4527fblanchette
added a few theorems about supremum in Ordered_Resolution_Prover 
May 8
9cc7791da210blanchette
added 'sublocale', simplified rest of formalization 
May 8
ec19eb9df9f6nipkow
tuned topics 
May 6
c50300e44852blanchette
added lemma to Ordered_Resolution_Prover 
May 6
cf6ff7e1b205blanchette
avoid mixture of definitionally equal constants 
May 6