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;
2015-11-10 wenzelm 2015-11-10 more thorough check_command, including completion;
2015-11-10 wenzelm 2015-11-10 clarified modules;
2015-11-10 wenzelm 2015-11-10 unused;
2015-11-10 wenzelm 2015-11-10 ignore pointless/unused options;
2015-11-10 wenzelm 2015-11-10 added document antiquotation @{theory_text}; tuned document;
2015-11-10 wenzelm 2015-11-10 allow open symboloid;
2015-11-10 fleury 2015-11-10 generalized so that is also works for veriT proofs
2015-11-10 fleury 2015-11-10 fixing premises in veriT proof reconstruction
2015-11-10 paulson 2015-11-10 Merge