15 hours ago paulson 2018-07-16 merged default tip
15 hours ago paulson 2018-07-16 de-applying and simplifying proofs
21 hours ago Manuel Eberl 2018-07-16 Tagged some more files in HOL-Analysis
24 hours ago Manuel Eberl 2018-07-16 Made simproc for sqrt/root of numeral more robust
31 hours ago Andreas Lochbihler 2018-07-16 merged
39 hours ago Andreas Lochbihler 2018-07-15 merged
39 hours ago Andreas Lochbihler 2018-07-15 more examples for Code_Lazy
40 hours ago paulson 2018-07-15 de-applying and meta-quantifying
44 hours ago paulson 2018-07-15 merged
44 hours ago paulson 2018-07-15 more renaming fixes
46 hours ago paulson 2018-07-15 fixes and more de-applying
2 days ago paulson 2018-07-15 more de-applying and a fix
2 days ago paulson 2018-07-15 merged
2 days ago paulson 2018-07-15 last bit of renaming
2 days ago paulson 2018-07-14 de-applying
2 days ago Manuel Eberl 2018-07-15 Added Real_Asymp package
2 days ago Wenda Li 2018-07-15 Tagged Conformal_Mappings in HOL-Analysis
3 days ago paulson 2018-07-13 merged
3 days ago paulson 2018-07-13 merged
3 days ago paulson 2018-07-13 de-applying
3 days ago Manuel Eberl 2018-07-13 HOL-Analysis: Volume of a simplex, Heron's theorem
3 days ago Manuel Eberl 2018-07-13 Tagged Ball_Volume and Gamma_Function in HOL-Analysis
3 days ago nipkow 2018-07-13 correct import
4 days ago nipkow 2018-07-13 merged
4 days ago nipkow 2018-07-13 unit_cube = cbox 0 One
4 days ago immler 2018-07-13 relaxed assumptions for dim_image_eq and dim_image_le
4 days ago paulson 2018-07-12 merged
4 days ago paulson 2018-07-12 de-applying (mostly Set_Interval)
5 days ago nipkow 2018-07-12 more economic tagging
5 days ago paulson 2018-07-11 de-applying (mostly Quotient)
5 days ago paulson 2018-07-11 de-applying
5 days ago paulson 2018-07-11 more de-applying
6 days ago paulson 2018-07-11 patched a continuity proof
6 days ago paulson 2018-07-11 merged
6 days ago paulson 2018-07-10 de-applying, etc.
6 days ago nipkow 2018-07-11 moved lemmas
7 days ago paulson 2018-07-10 merged
7 days ago paulson 2018-07-09 final removal of smt from Algebra
7 days ago immler 2018-07-10 make theorem, corollary, and proposition %important for HOL-Analysis manual
7 days ago paulson 2018-07-09 removal of smt and certain refinements
8 days ago paulson 2018-07-08 removal of smt
8 days ago paulson 2018-07-08 elimination of some "smt"
9 days ago paulson 2018-07-08 De-applying
9 days ago paulson 2018-07-07 merged
9 days ago paulson 2018-07-07 de-applying, etc.
10 days ago nipkow 2018-07-06 more symmetric
10 days ago wenzelm 2018-07-06 prefer HTTPS;
10 days ago wenzelm 2018-07-06 just one global lock for group status: avoid proliferation of mutexes, condvars;
11 days ago wenzelm 2018-07-06 more frugal assignment of lazy value: fewer mutexes, condvars; cannot use RunCall.clearMutableBit due to spurious crashes;
11 days ago paulson 2018-07-06 replaced subgroup_imp_subset in Modules
11 days ago paulson 2018-07-05 merged
11 days ago paulson 2018-07-05 de-applying
11 days ago paulson 2018-07-05 merged
11 days ago paulson 2018-07-05 submodules
11 days ago wenzelm 2018-07-05 more manual tests;
11 days ago wenzelm 2018-07-05 store immutable result: fewer refs, mutexes, condvars;
12 days ago wenzelm 2018-07-04 more frugal single-assignment according to David Matthews: dispose mutable lock/cond eventually;
13 days ago Lars Hupel 2018-07-04 merged
13 days ago Lars Hupel 2018-07-04 avoid clashes in quickcheck [random]
13 days ago paulson 2018-07-04 infinite products: the final piece