6 hours ago nipkow 2019-04-18 added lemma default tip
14 hours ago haftmann 2019-04-18 incorporated various material from the AFP into the distribution
28 hours ago haftmann 2019-04-17 backed out experimental b67bab2b132c, which slipped in accidentally
16 hours ago nipkow 2019-04-18 merged
25 hours ago nipkow 2019-04-17 added lemmas
24 hours ago paulson 2019-04-17 moved subset_image_inj into Hilbert_Choice
28 hours ago paulson 2019-04-17 Lindelöf spaces and supporting material
2 days ago haftmann 2019-04-16 hierarchically inclusive named theorem collections
2 days ago haftmann 2019-04-16 removed unused fact collections
2 days ago haftmann 2019-04-16 eliminated type class
2 days ago haftmann 2019-04-16 entry point for comprehensive word library
2 days ago haftmann 2019-04-16 tuned theory names
2 days ago haftmann 2019-04-16 integrated Bit_Comparison into Word corpus
2 days ago haftmann 2019-04-16 tuned
2 days ago haftmann 2019-04-16 prefer one theory for misc material
2 days ago haftmann 2019-04-16 moved instance to appropriate place
2 days ago wenzelm 2019-04-16 tuned for release;
2 days ago wenzelm 2019-04-16 clarified goto_file (again): treat bad entry as plain file to open empty buffer instead of error (amending a8142ac5e4b6);
4 days ago wenzelm 2019-04-14 afford more examples;
4 days ago wenzelm 2019-04-14 obsolete -- this is quite fast;
4 days ago paulson 2019-04-14 Group theory developments towards proving algebraic closure (by de Vilhena and Baillon)
4 days ago paulson 2019-04-14 merged
4 days ago paulson 2019-04-14 markup fixes
5 days ago paulson 2019-04-13 merged
5 days ago paulson 2019-04-13 Towards a proof of algebraic closure (NB not finished)
5 days ago wenzelm 2019-04-13 tuned signature;
5 days ago wenzelm 2019-04-13 prefer ctyp operations;
5 days ago wenzelm 2019-04-13 meson: more cterm operations;
5 days ago wenzelm 2019-04-13 more ctyp operations;
5 days ago wenzelm 2019-04-13 tuned;
5 days ago wenzelm 2019-04-13 clarified: use existing Thm.dest_ctyp_fun (which is more strict);
5 days ago wenzelm 2019-04-13 prefer exception TYPE, e.g. when used within conversion;
5 days ago wenzelm 2019-04-13 tuned signature -- more ctyp operations;
5 days ago wenzelm 2019-04-13 clarified group of "main" library sessions;
5 days ago wenzelm 2019-04-13 tuned signature -- more ctyp operations;
5 days ago wenzelm 2019-04-13 merged
5 days ago wenzelm 2019-04-13 tuned signature: more operations;
5 days ago haftmann 2019-04-13 backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is
5 days ago haftmann 2019-04-13 tuned
5 days ago haftmann 2019-04-13 more document structure
5 days ago haftmann 2019-04-13 tuned
5 days ago wenzelm 2019-04-13 more abbrevs;
5 days ago wenzelm 2019-04-13 obsolete;
5 days ago wenzelm 2019-04-12 merged
6 days ago wenzelm 2019-04-12 updated documentation;
6 days ago wenzelm 2019-04-12 avoid Isabelle symbols in URL;
6 days ago wenzelm 2019-04-12 formal URLs;
6 days ago wenzelm 2019-04-12 tuned spacing;
6 days ago wenzelm 2019-04-12 modernized tags: default scope excludes proof;
6 days ago wenzelm 2019-04-12 report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
6 days ago wenzelm 2019-04-12 support "tag" marker with scope;
6 days ago paulson 2019-04-12 tidying up messy proofs about group element order
6 days ago paulson 2019-04-11 merged
6 days ago paulson 2019-04-11 simpler and stronger proofs
7 days ago wenzelm 2019-04-11 tuned;
7 days ago wenzelm 2019-04-11 tuned;
7 days ago paulson 2019-04-11 merge plus tidied three proofs
7 days ago paulson 2019-04-11 merged
7 days ago paulson 2019-04-11 merged
7 days ago paulson 2019-04-11 type instantiations for poly_mapping as a real_normed_vector