2018-05-04 wenzelm no censorship of view title;
2018-05-04 wenzelm set view title dynamically;
2018-05-04 nipkow tuned
2018-05-04 nipkow tuned
2018-05-03 paulson Some tidying up (mostly regarding summations from 0)
2018-05-03 paulson tidied up Infinite_Products
2018-05-03 immler merged
2018-05-03 immler fixed HOL-Analysis
2018-05-03 immler merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
2018-05-02 immler added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
2018-05-03 paulson a lemma about infinite products
2018-05-02 paulson merged
2018-05-02 paulson tidying up and using real induction methods
2018-05-02 wenzelm tuned -- slightly smaller future closure size;
2018-05-02 wenzelm clarified menu actions;
2018-05-02 wenzelm purge history more thoroughly (see also 3156faac30a7);
2018-05-02 paulson merged
2018-05-02 paulson type class generalisations; some work on infinite products
2018-05-02 paulson merged
2018-05-01 paulson simplified some messy proofs
2018-05-01 wenzelm clarified theory location and imports: avoid surprises due to Pure instead of Main (e.g. simpset operations);
2018-05-01 wenzelm avoid output showing up in kill ring (via TextArea.setText, JEditBuffer.remove, UndoManager.contentRemoved), e.g. relevant for action "paste-deleted";
2018-04-30 paulson merged
2018-04-30 paulson more general tidying up
2018-04-30 boehmes prefer explicit error message to unspecific Options exception: Z3 proof traces may lack information necessary for replay when dealing with quantified formulas
2018-04-29 paulson cleaned up more messy proofs
2018-04-29 paulson more defer/prefer
2018-04-28 paulson getting rid of more "defer", etc.
2018-04-28 paulson getting rid of "defer"
2018-04-27 paulson another big cleanup
2018-04-27 paulson merged
2018-04-27 paulson minor typeclass generalisations and junk removal
2018-04-26 paulson merged
2018-04-26 paulson more messy proofs
2018-04-26 nipkow merged
2018-04-26 nipkow new simp modifier: reorient
2018-04-26 paulson small typeclass generalisations
2018-04-26 paulson merged
2018-04-26 paulson some of Jose Divasón's material from Rank_Nullity_Theorem/Miscellaneous
2018-04-26 wenzelm spelling;
2018-04-25 paulson more messy proofs redone, and new material
2018-04-25 paulson merged
2018-04-25 paulson merged
2018-04-25 paulson new material on matricies by Tim Makarios (from Tarskis_Geometry in the AFP)
2018-04-25 wenzelm merged
2018-04-25 wenzelm tuned -- avoid spurious exception trace for "the";
2018-04-25 haftmann proof of concept for residue rings over int using type numerals
2018-04-25 haftmann more correct error message
2018-04-25 haftmann uniform tagging for printable and non-printable literals
2018-04-24 paulson merged
2018-04-24 paulson fixing more messy proofs
2018-04-24 wenzelm more ambitious parallelism (in contrast to a8ee8e4884ec): pri = 1 ensures that internal proof tasks are executed before the already forked theory outline with pri = 0;
2018-04-24 wenzelm eliminated pointless special case (see also a8ee8e4884ec, c4c4c2f01723);
2018-04-24 haftmann proper datatype for 8-bit characters
2018-04-24 haftmann corrected nonsense
2018-04-24 wenzelm less ambitious parallelism: avoid problems with HOL-Proofs and threads=2 (congestion with many thousands futures and rather dense heap);
2018-04-24 wenzelm clarified modules;
2018-04-23 paulson tidied some horrid proofs
2018-04-23 nipkow del_max -> split_max
2018-04-22 paulson Tidied a lot of messy proofs
2018-04-21 nipkow dont rename PQ.del_min
2018-04-21 nipkow del_min -> split_min
2018-04-20 wenzelm merged
2018-04-20 wenzelm support for XZ.Cache;
(0) -30000 -10000 -3000 -1000 -300 -100 -64 +64 +100 +300 +1000 +3000 +10000 tip