2015-12-17 wenzelm 2015-12-17 support pretty break indent, like underlying ML systems;
2015-12-19 blanchet 2015-12-19 register record functions as 'Spec_Rules'
2015-12-19 blanchet 2015-12-19 cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer
2015-12-19 blanchet 2015-12-19 removed subsumed dependency
2015-12-19 blanchet 2015-12-19 removed dead code
2015-12-18 Andreas Lochbihler 2015-12-18 add serialisation for abs on integer to target language operation
2015-12-18 Andreas Lochbihler 2015-12-18 add gcd instance for integer and serialisation to target language operations
2015-12-16 wenzelm 2015-12-16 merged
2015-12-16 wenzelm 2015-12-16 tuned whitespace;
2015-12-16 wenzelm 2015-12-16 rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
2015-12-15 wenzelm 2015-12-15 tuned signature -- clarified modules;
2015-12-15 wenzelm 2015-12-15 unused;
2015-12-15 wenzelm 2015-12-15 unused;
2015-12-15 paulson 2015-12-15 Merge
2015-12-15 paulson 2015-12-15 New complex analysis material
2015-11-25 hoelzl 2015-11-25 infix syntax for measurable set
2015-12-14 wenzelm 2015-12-14 more standard term equality;
2015-12-14 wenzelm 2015-12-14 tuned;
2015-12-14 wenzelm 2015-12-14 tuned signature;
2015-12-14 wenzelm 2015-12-14 tuned message;
2015-12-13 wenzelm 2015-12-13 merged
2015-12-13 wenzelm 2015-12-13 more general types Proof.method / context_tactic; proper context for Method.insert_tac; tuned;
2015-12-12 wenzelm 2015-12-12 tuned;
2015-12-12 wenzelm 2015-12-12 clarified ML scopes; tuned;
2015-12-12 wenzelm 2015-12-12 clarified ML scopes;
2015-12-12 wenzelm 2015-12-12 tuned;
2015-12-12 wenzelm 2015-12-12 unused;
2015-12-12 wenzelm 2015-12-12 tuned;
2015-12-11 wenzelm 2015-12-11 clarified modules;
2015-12-12 haftmann 2015-12-12 modernized
2015-12-12 haftmann 2015-12-12 modernized
2015-12-11 haftmann 2015-12-11 modernized
2015-12-10 wenzelm 2015-12-10 isabelle update_cartouches -c -t;
2015-12-10 wenzelm 2015-12-10 proper checksum for cygwin-20151210.tar.gz (some snapshot after 1.7.35-1);
2015-12-10 wenzelm 2015-12-10 avoid application spurious startup error;
2015-12-10 wenzelm 2015-12-10 current Cygwin snapshot in preparation of release;
2015-12-10 wenzelm 2015-12-10 hardwired LANG, to avoid sporadic surprises with local environments;
2015-12-10 wenzelm 2015-12-10 make SML/NJ happy;
2015-12-10 paulson 2015-12-10 not_leE -> not_le_imp_less and other tidying
2015-12-07 haftmann 2015-12-07 clarified terminology
2015-12-09 wenzelm 2015-12-09 tuned;
2015-12-09 wenzelm 2015-12-09 tuned signature;
2015-12-09 wenzelm 2015-12-09 tuned signature;
2015-12-09 wenzelm 2015-12-09 tuned;
2015-12-09 wenzelm 2015-12-09 more direct use of Token.src as token list; tuned signature; tuned;
2015-12-09 wenzelm 2015-12-09 merged
2015-12-09 wenzelm 2015-12-09 unused;
2015-12-09 wenzelm 2015-12-09 merged
2015-12-09 wenzelm 2015-12-09 clarified type Token.src: plain token list, with usual implicit value assignment; clarified type Token.name_value, notably for head of Token.src; clarified Attrib/Method check_src vs. parser;
2015-12-09 wenzelm 2015-12-09 tuned;
2015-12-08 wenzelm 2015-12-08 tuned;
2015-12-08 wenzelm 2015-12-08 added Proof_Context.add_thms_dynamic, which is potentially useful for Eisbach;
2015-12-09 paulson 2015-12-09 sorted out eventually_mono
2015-12-08 nipkow 2015-12-08 tightened invariant
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-12-07 paulson 2015-12-07 Merge
2015-12-07 paulson 2015-12-07 Cauchy's integral formula for circles. Starting to fix eventually_mono.
2015-12-07 eberlm 2015-12-07 Merged
2015-12-07 eberlm 2015-12-07 Generalised derivative rule for division on formal power series
2015-12-07 wenzelm 2015-12-07 tuned;