HomePhabricator

merge from AFP 2019

Description

merge from AFP 2019

Event Timeline

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