HomeIsabelle/Phabricator

merge from AFP 2019

Description

merge from AFP 2019

Event Timeline

Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPe10739c4e48f: merge from AFP 2019.Dec 2 2019, 12:58 PM

Merged Changes

This commit merges a very large number of changes. Only the first 50 are shown.
CommitAuthorDetailsCommitted
e30fe5fba4d7pruvisto
Merged 
Dec 2 2019
4f482d20a008pruvisto
adapted to isabelle-dev 954ee5acaae0 
Nov 30 2019
e8bc925a7952Wenda Li
adapted to Isabelle/0c47c128f9af; 
Dec 2 2019
7e45833c40f6haftmann
explicit variable declaration 
Nov 29 2019
78025c98b739wenzelm
adapted to Isabelle/592e2afdd50c; 
Nov 29 2019
6128683958cawenzelm
more realistic timeout; 
Nov 27 2019
c47ca19eaae3haftmann
proper prefix syntax 
Nov 22 2019
7e7b23d02d4bhaftmann
removed unused auxiliary lemmas 
Nov 22 2019
87c3943758c0Manuel Eberl
More about Bernoulli numbers 
Nov 17 2019
5580004cc074Manuel Eberl
Added von Staudt–Clausen theorem to Bernoulli 
Nov 14 2019
f1ef07c47429Lars Hupel
don't build Linear_Programming on Mac 
Nov 10 2019
54f6a4f1d8a3nipkow
updated to fdb6c5034c24 
Nov 5 2019
2a06a089800fimmler
merged 
Nov 5 2019
c5944c920143immler
moved Interval and Interval_Approximation to isabelle 
Nov 5 2019
3f2bdb753c38paulson
patched a proof 
Nov 5 2019
c5c88012f116paulson
fixed a failing (and ugly) proof 
Nov 2 2019
1f17a5f5a1e2Andreas Halkjær From
Merge branch 
Oct 31 2019
f05300d8017aAndreas Halkjær From
Tuned spacing. 
Oct 31 2019
877fab13602enipkow
follow devel changeset 581083959358 
Oct 27 2019
1a0be182fddaAndreas Halkjær From
Consistent spacing in set comprehension and name fixes. 
Oct 25 2019
616e41c5089cAndreas Halkjær From
Consistent spacing in set comprehension. 
Oct 25 2019
ba01b2eda5e4nipkow
updated email 
Oct 24 2019
c85fcabd5bffwenzelm
avoid name clash of internal derivations; 
Oct 21 2019
9bd3fa01955awenzelm
recovered proof; 
Oct 21 2019
6a3c69467146kleing
Clean: ROOT/directories structure 
Oct 21 2019
2ac9ae9dd0f6kleing
Clean: consolidate ROOT file for new session directories 
Oct 20 2019
48295c330a18kleing
merge from afp-2019 
Oct 20 2019
c7faf745010fhaftmann
moved quickcheck setup to distribution 
Oct 18 2019
c30a1164293ahaftmann
moved generic instance to distribution 
Oct 18 2019
02b9d0561118wenzelm
recovered proofs; 
Oct 15 2019
e92e80d9cb16Julian Brunner
made NBA translation explicit 
Oct 14 2019
f9adabfbcca6Giuliano Losa
merge 
Oct 11 2019
dd760b1d41e5Giuliano Losa
add a section about Stellar's intact sets 
Oct 11 2019
2382848477eaGiuliano Losa
Add lemma strong_cluster_union 
Oct 11 2019
93099fba4c66Giuliano Losa
Remove spurious W variable in locale assumption 
Sep 26 2019
381f2aa05ed3haftmann
avoid sign_simps in favour of algebra_split_simps 
Oct 9 2019
12ac7c824ad0paulson
Moved some lemmas about limits to Complex_Main 
Oct 9 2019
d7a872772538haftmann
formally augmented corresponding rules for field_simps 
Oct 8 2019
ab79744bf7a0Julian Brunner
updated to work with recent automata changes 
Oct 8 2019
83c109099c9bJulian Brunner
added NGBA implementations 
Oct 8 2019
a0ad86208e23Julian Brunner
adjusted NBA implementation 
Oct 8 2019
a7cac9b35489Julian Brunner
added NBA combination nodes theorems, minor adjustments 
Oct 8 2019
dfe6b2a998fewenzelm
refer to explicit ISABELLE_DOT instead of implicit PATH; 
Oct 7 2019
dfa7db541b8ewenzelm
avoid name clash of internal derivations; 
Oct 4 2019
1f139e059475wenzelm
avoid name clash of internal derivations; 
Oct 4 2019
29b3e29e042ewenzelm
proper Consts.dummy_types; 
Oct 4 2019
dcb063b90519nipkow
updated to devel 
Sep 26 2019
66bfe59e1850paulson
Moving a bit more material into the Analysis library 
Sep 26 2019
c3a70e5ad56bpaulson
Removal of material now in Isabelle's libraries 
Sep 25 2019
ee2ef0deb899nipkow
updated to devel 
Sep 25 2019