22 months ago paulson <lp15@cam.ac.uk> [Thu, 24 Aug 2017 17:15:53 +0100] rev 66503
more elimination of "guess", etc.
src/HOL/Analysis/Henstock_Kurzweil_Integration.thy src/HOL/Analysis/Linear_Algebra.thy

22 months ago nipkow [Fri, 25 Aug 2017 08:59:54 +0200] rev 66502
Added lemmas
src/HOL/List.thy

22 months ago haftmann [Thu, 24 Aug 2017 17:41:49 +0200] rev 66501
swapping of theory dependency yields less pervasive syntax requiring popular symbols \<mu>, \<nu>
src/HOL/Algebra/Complete_Lattice.thy src/HOL/Algebra/Divisibility.thy src/HOL/Algebra/Group.thy

22 months ago haftmann [Thu, 24 Aug 2017 17:24:12 +0200] rev 66500
more correct output syntax declaration
src/HOL/Algebra/Multiplicative_Group.thy

22 months ago nipkow [Thu, 24 Aug 2017 21:56:26 +0200] rev 66499
tuned
src/HOL/Data_Structures/Base_FDS.thy src/HOL/Data_Structures/Leftist_Heap.thy

22 months ago paulson <lp15@cam.ac.uk> [Thu, 24 Aug 2017 12:45:46 +0100] rev 66498
Merge (non-trivial)
src/HOL/Analysis/Henstock_Kurzweil_Integration.thy src/HOL/Analysis/Tagged_Division.thy

22 months ago paulson <lp15@cam.ac.uk> [Wed, 23 Aug 2017 23:46:35 +0100] rev 66497
More tidying, and renaming of theorems
src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy src/HOL/Analysis/Henstock_Kurzweil_Integration.thy src/HOL/Analysis/Improper_Integral.thy src/HOL/Analysis/Tagged_Division.thy

22 months ago paulson [Wed, 23 Aug 2017 19:54:30 +0100] rev 66496
merged

22 months ago paulson <lp15@cam.ac.uk> [Wed, 23 Aug 2017 19:54:11 +0100] rev 66495
More tidying up of monotone_convergence_interval
src/HOL/Analysis/Harmonic_Numbers.thy src/HOL/Analysis/Henstock_Kurzweil_Integration.thy

22 months ago blanchet [Thu, 24 Aug 2017 10:47:56 +0200] rev 66494
tuning (proofs and code)
src/HOL/Library/Multiset.thy src/HOL/Tools/BNF/bnf_lfp_size.ML