2015-11-15 nipkow 2015-11-15 tuned white space
2015-11-15 haftmann 2015-11-15 leftover from 27ca6147e3b3
2015-11-15 haftmann 2015-11-15 tuned whitespace
2015-11-15 haftmann 2015-11-15 NEWS
2015-11-15 haftmann 2015-11-15 droppen diagnostic junk from 4b53042d7a40
2015-11-14 haftmann 2015-11-14 represent both algebraic and local-theory views on locale interpretation in interfaces
2015-11-14 haftmann 2015-11-14 tuned -- share implementations as far as appropriate
2015-11-14 haftmann 2015-11-14 prefer "rewrites" and "defines" to note rewrite morphisms
2015-11-14 haftmann 2015-11-14 coalesce permanent_interpretation.ML with interpretation.ML
2015-11-14 haftmann 2015-11-14 separate ML module for interpretation
2015-11-14 haftmann 2015-11-14 reverted half-baken 7d1127ac2251
2015-11-14 haftmann 2015-11-14 explicit computation of sort arguments for code equations makes less assumption about sort arguments of underlying type class instances
2015-11-14 wenzelm 2015-11-14 more standard ML, to make SML/NJ more happy;
2015-11-13 wenzelm 2015-11-13 tuned;
2015-11-13 wenzelm 2015-11-13 tuned whitespace;
2015-11-13 wenzelm 2015-11-13 tuned;
2015-11-13 wenzelm 2015-11-13 tuned whitespace;
2015-11-13 wenzelm 2015-11-13 merged
2015-11-13 wenzelm 2015-11-13 added antiquotation @{doc}, e.g. useful for demonstration purposes;
2015-11-13 wenzelm 2015-11-13 preserve names of for-fixes for faithfully;
2015-11-13 wenzelm 2015-11-13 more documentation;
2015-11-13 wenzelm 2015-11-13 tuned whitespace;
2015-11-13 wenzelm 2015-11-13 more uniform jEdit properties;
2015-11-13 wenzelm 2015-11-13 avoid vacuous quantification, as usual for shared variable scope;
2015-11-13 wenzelm 2015-11-13 support for structure statements in 'assume', 'presume';
2015-11-12 wenzelm 2015-11-12 support short form for \<^theory_text>;
2015-11-13 paulson 2015-11-13 MIR decision procedure again working
2015-11-13 nipkow 2015-11-13 unnecessary precondition
2015-11-13 paulson 2015-11-13 Merge
2015-11-13 paulson 2015-11-13 Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
2015-11-13 nipkow 2015-11-13 tuned name
2015-11-13 nipkow 2015-11-13 tuned
2015-11-12 blanchet 2015-11-12 use cartouches instead of backquotes
2015-11-12 nipkow 2015-11-12 translation for conjunctive premises
2015-11-12 nipkow 2015-11-12 tuned
2015-11-12 nipkow 2015-11-12 added proof state output warning
2015-11-11 nipkow 2015-11-11 tuned
2015-11-11 nipkow 2015-11-11 merged
2015-11-11 nipkow 2015-11-11 no CRLF
2015-11-11 paulson 2015-11-11 new conversion theorems for int, nat to float
2015-11-11 nipkow 2015-11-11 merged
2015-11-11 nipkow 2015-11-11 uniform proof of lemmas
2015-11-11 Andreas Lochbihler 2015-11-11 merged
2015-11-11 Andreas Lochbihler 2015-11-11 adapt to 90f54d9e63f2
2015-11-11 Andreas Lochbihler 2015-11-11 add various lemmas
2015-11-11 Andreas Lochbihler 2015-11-11 add lemmas
2015-11-11 Andreas Lochbihler 2015-11-11 generalise lemma
2015-11-11 Andreas Lochbihler 2015-11-11 add lemmas for extended nats and reals
2015-11-11 Andreas Lochbihler 2015-11-11 add various lemmas
2015-11-11 Andreas Lochbihler 2015-11-11 cancel complementary terms as arguments to sup/inf in boolean algebras
2015-11-11 Andreas Lochbihler 2015-11-11 add lemmas about monoids and groups
2015-11-11 nipkow 2015-11-11 tuned
2015-11-10 wenzelm 2015-11-10 recovered from a9c0572109af;
2015-11-10 wenzelm 2015-11-10 merged
2015-11-10 wenzelm 2015-11-10 tuned whitespace;
2015-11-10 wenzelm 2015-11-10 added @{command}, @{method}, @{attribute};
2015-11-10 wenzelm 2015-11-10 smart quoting of non-identifiers, e.g. jEdit actions;
2015-11-10 wenzelm 2015-11-10 more thorough check_action, including completion;
2015-11-10 wenzelm 2015-11-10 tuned signature;
2015-11-10 wenzelm 2015-11-10 clarified modules;