115 minutes ago blanchet 2018-07-20 don't lose facts that were introduced to deal with a theory or some preprocessing in the prover (e.g. the definition of 'abs' in an SMT proof) default tip
14 hours ago Andreas Lochbihler 2018-07-20 add lemmas about prod_filter
15 hours ago paulson 2018-07-20 merged
23 hours ago paulson 2018-07-20 corrections to markup
24 hours ago paulson 2018-07-19 updated material concerning Algebra
30 hours ago paulson 2018-07-19 merged
30 hours ago paulson 2018-07-19 de-applying
21 hours ago wenzelm 2018-07-20 added system option "strict_facts";
2 days ago haftmann 2018-07-18 slightly more canonical imports
2 days ago haftmann 2018-07-18 setup for Haskell taken over from AFP / Gauss_Jordan
2 days ago haftmann 2018-07-18 tuned equation
2 days ago haftmann 2018-07-18 restructured for future incorporation of Haskell
2 days ago haftmann 2018-07-18 slightly more uniform style
2 days ago haftmann 2018-07-18 taken over from AFP / Gauss_Jordan
2 days ago haftmann 2018-07-18 more cartouches
37 hours ago traytel 2018-07-19 merged
38 hours ago traytel 2018-07-19 normalize imports
3 days ago Manuel Eberl 2018-07-17 tagged
2 days ago wenzelm 2018-07-18 evade odd connection problems to https://isabelle.in.tum.de from some remote hosts;
2 days ago wenzelm 2018-07-18 prefer HTTPS;
2 days ago wenzelm 2018-07-18 more ANNOUNCE;
2 days ago wenzelm 2018-07-18 tuned;
3 days ago paulson 2018-07-17 more de-applying
3 days ago paulson 2018-07-16 merged
3 days ago paulson 2018-07-16 de-applying and simplifying proofs
4 days ago Manuel Eberl 2018-07-16 Tagged some more files in HOL-Analysis
4 days ago Manuel Eberl 2018-07-16 Made simproc for sqrt/root of numeral more robust
4 days ago Andreas Lochbihler 2018-07-16 merged
5 days ago Andreas Lochbihler 2018-07-15 merged
5 days ago Andreas Lochbihler 2018-07-15 more examples for Code_Lazy
5 days ago paulson 2018-07-15 de-applying and meta-quantifying
5 days ago paulson 2018-07-15 merged
5 days ago paulson 2018-07-15 more renaming fixes
5 days ago paulson 2018-07-15 fixes and more de-applying
5 days ago paulson 2018-07-15 more de-applying and a fix
5 days ago paulson 2018-07-15 merged
5 days ago paulson 2018-07-15 last bit of renaming
6 days ago paulson 2018-07-14 de-applying
5 days ago Manuel Eberl 2018-07-15 Added Real_Asymp package
5 days ago Wenda Li 2018-07-15 Tagged Conformal_Mappings in HOL-Analysis
7 days ago paulson 2018-07-13 merged
7 days ago paulson 2018-07-13 merged
7 days ago paulson 2018-07-13 de-applying
7 days ago Manuel Eberl 2018-07-13 HOL-Analysis: Volume of a simplex, Heron's theorem
7 days ago Manuel Eberl 2018-07-13 Tagged Ball_Volume and Gamma_Function in HOL-Analysis
7 days ago nipkow 2018-07-13 correct import
7 days ago nipkow 2018-07-13 merged
7 days ago nipkow 2018-07-13 unit_cube = cbox 0 One
7 days ago immler 2018-07-13 relaxed assumptions for dim_image_eq and dim_image_le
8 days ago paulson 2018-07-12 merged
8 days ago paulson 2018-07-12 de-applying (mostly Set_Interval)
8 days ago nipkow 2018-07-12 more economic tagging
8 days ago paulson 2018-07-11 de-applying (mostly Quotient)
9 days ago paulson 2018-07-11 de-applying
9 days ago paulson 2018-07-11 more de-applying
9 days ago paulson 2018-07-11 patched a continuity proof
9 days ago paulson 2018-07-11 merged
9 days ago paulson 2018-07-10 de-applying, etc.
9 days ago nipkow 2018-07-11 moved lemmas
10 days ago paulson 2018-07-10 merged