18 months ago Andreas Lochbihler 2018-07-15 more examples for Code_Lazy
18 months ago paulson 2018-07-15 de-applying and meta-quantifying
18 months ago paulson 2018-07-15 merged
18 months ago paulson 2018-07-15 more renaming fixes
18 months ago paulson 2018-07-15 fixes and more de-applying
18 months ago paulson 2018-07-15 more de-applying and a fix
18 months ago paulson 2018-07-15 merged
18 months ago paulson 2018-07-15 last bit of renaming
18 months ago paulson 2018-07-14 de-applying
18 months ago Manuel Eberl 2018-07-15 Added Real_Asymp package
18 months ago Wenda Li 2018-07-15 Tagged Conformal_Mappings in HOL-Analysis
18 months ago paulson 2018-07-13 merged
18 months ago paulson 2018-07-13 merged
18 months ago paulson 2018-07-13 de-applying
18 months ago Manuel Eberl 2018-07-13 HOL-Analysis: Volume of a simplex, Heron's theorem
18 months ago Manuel Eberl 2018-07-13 Tagged Ball_Volume and Gamma_Function in HOL-Analysis
18 months ago nipkow 2018-07-13 correct import
18 months ago nipkow 2018-07-13 merged
18 months ago nipkow 2018-07-13 unit_cube = cbox 0 One
18 months ago immler 2018-07-13 relaxed assumptions for dim_image_eq and dim_image_le
18 months ago paulson 2018-07-12 merged
18 months ago paulson 2018-07-12 de-applying (mostly Set_Interval)
18 months ago nipkow 2018-07-12 more economic tagging
18 months ago paulson 2018-07-11 de-applying (mostly Quotient)
18 months ago paulson 2018-07-11 de-applying
18 months ago paulson 2018-07-11 more de-applying
18 months ago paulson 2018-07-11 patched a continuity proof
18 months ago paulson 2018-07-11 merged
18 months ago paulson 2018-07-10 de-applying, etc.
18 months ago nipkow 2018-07-11 moved lemmas
18 months ago paulson 2018-07-10 merged
18 months ago paulson 2018-07-09 final removal of smt from Algebra
18 months ago immler 2018-07-10 make theorem, corollary, and proposition %important for HOL-Analysis manual
18 months ago paulson 2018-07-09 removal of smt and certain refinements
18 months ago paulson 2018-07-08 removal of smt
18 months ago paulson 2018-07-08 elimination of some "smt"
18 months ago paulson 2018-07-08 De-applying
18 months ago paulson 2018-07-07 merged
18 months ago paulson 2018-07-07 de-applying, etc.
18 months ago nipkow 2018-07-06 more symmetric
18 months ago wenzelm 2018-07-06 prefer HTTPS;
18 months ago wenzelm 2018-07-06 just one global lock for group status: avoid proliferation of mutexes, condvars;
18 months ago wenzelm 2018-07-06 more frugal assignment of lazy value: fewer mutexes, condvars; cannot use RunCall.clearMutableBit due to spurious crashes;
18 months ago paulson 2018-07-06 replaced subgroup_imp_subset in Modules
18 months ago paulson 2018-07-05 merged
18 months ago paulson 2018-07-05 de-applying
18 months ago paulson 2018-07-05 merged
18 months ago paulson 2018-07-05 submodules
18 months ago wenzelm 2018-07-05 more manual tests;
18 months ago wenzelm 2018-07-05 store immutable result: fewer refs, mutexes, condvars;
18 months ago wenzelm 2018-07-04 more frugal single-assignment according to David Matthews: dispose mutable lock/cond eventually;
18 months ago Lars Hupel 2018-07-04 merged
18 months ago Lars Hupel 2018-07-04 avoid clashes in quickcheck [random]
18 months ago paulson 2018-07-04 infinite products: the final piece
18 months ago paulson 2018-07-03 more on infinite products
18 months ago paulson 2018-07-03 merged
18 months ago paulson 2018-07-03 even more from Paulo
18 months ago wenzelm 2018-07-03 more standard headers; tuned whitespace;
18 months ago wenzelm 2018-07-03 eliminated hard TABs, assuming tabsize=8;
18 months ago paulson 2018-07-03 more latex problems