2014-04-05 haftmann 2014-04-05 CONTRIBUTORS
2014-04-05 haftmann 2014-04-05 proper inclusion into library
2014-04-05 paulson 2014-04-05 A single [simp] to handle the case -a/-b.
2014-04-04 wenzelm 2014-04-04 support for jEdit Navigator plugin;
2014-04-04 wenzelm 2014-04-04 more permissive Session.update_options: this is wired to jEdit PropertiesChanged, which may occur before the prover is started;
2014-04-04 blanchet 2014-04-04 added option to Mirabelle
2014-04-04 paulson 2014-04-04 divide_minus_left divide_minus_right are in field_simps but are not default simprules
2014-04-03 paulson 2014-04-03 removing simprule status for divide_minus_left and divide_minus_right
2014-04-04 wenzelm 2014-04-04 merged;
2014-04-04 wenzelm 2014-04-04 tuned rendering -- take 1px line border into account;
2014-04-04 wenzelm 2014-04-04 revert ce37fcb30cf2 for the sake of Mac OS X -- let some event listeners of jEdit reset the cursor;
2014-04-04 wenzelm 2014-04-04 tuned white space;
2014-04-04 blanchet 2014-04-04 use Z3 TPTP cores rather than proofs since the latter are somewhat broken
2014-04-04 blanchet 2014-04-04 tuned spaces
2014-04-04 Andreas Lochbihler 2014-04-04 merged
2014-04-04 Andreas Lochbihler 2014-04-04 add missing adaptation for narrowing to work with variables of type integer => integer
2014-04-04 wenzelm 2014-04-04 merged
2014-04-04 wenzelm 2014-04-04 added ML antiquotation @{print};
2014-04-04 wenzelm 2014-04-04 afford larger full_index, to save a few milliseconds during rendering (notably text_overview);
2014-04-04 blanchet 2014-04-04 improved parsing of "z3_tptp" proofs
2014-04-03 wenzelm 2014-04-03 merged
2014-04-03 wenzelm 2014-04-03 more direct warning within persistent Protocol.Status; consider Markup.ERROR (e.g. from Output.error_message without exception) as failure; tuned;
2014-04-03 wenzelm 2014-04-03 clarified Version.syntax -- avoid guessing initial situation;
2014-04-03 wenzelm 2014-04-03 more abstract Prover.Syntax, as proposed by Carst Tankink;
2014-04-03 wenzelm 2014-04-03 tuned signature (see also 0850d43cb355);
2014-04-03 wenzelm 2014-04-03 slightly more readable protocol trace (NB1: prover input is always marked as <prover_command/>; NB2: adding indentation would invalidate the XML);
2014-04-03 wenzelm 2014-04-03 recovered public command_line from d92eb5c3960d, which is important for alternative prover processes;
2014-04-03 wenzelm 2014-04-03 tuned rendering for 5 different look-and-feels;
2014-04-03 wenzelm 2014-04-03 more symbol abbrevs, e.g. relevant for list comprehension in HOL/List.thy or HOL/Library/Monad_Syntax.thy;
2014-04-03 wenzelm 2014-04-03 more general prover operations;
2014-04-03 wenzelm 2014-04-03 tuned signature -- pro forma;
2014-04-03 wenzelm 2014-04-03 more general prover operations;
2014-04-03 paulson 2014-04-03 Merge
2014-04-03 paulson 2014-04-03 Cleaned up some messy proofs
2014-04-03 hoelzl 2014-04-03 fix #0556204bc230
2014-04-03 hoelzl 2014-04-03 merged DERIV_intros, has_derivative_intros into derivative_intros
2014-04-03 blanchet 2014-04-03 don't pass Vampire option that doesn't exist anymore (and that wasn't strictly necessary with older Vampires)
2014-04-03 blanchet 2014-04-03 use Alt-Ergo 0.95.2, the latest and greatest version
2014-04-03 blanchet 2014-04-03 updated Z3 TPTP to 4.3.1+
2014-04-03 blanchet 2014-04-03 updated Why3 version in docs
2014-04-03 blanchet 2014-04-03 added same idiomatic handling of namings for Ctr_Sugar/BNF-related interpretation hooks as for typedef and (old-style) datatypes
2014-04-03 blanchet 2014-04-03 use same idiom as used for datatype 'size' function to name constants and theorems emerging from various type interpretations -- reduces the chances of name clashes on theory merges
2014-04-03 blanchet 2014-04-03 removed clone (cf. 300f613060b0)
2014-04-02 wenzelm 2014-04-02 tuned signature -- more explicit iterator terminology;
2014-04-02 wenzelm 2014-04-02 more explicit iterator terminology, in accordance to Scala 2.8 library; clarified Graph.keys_iterator vs. Graph.keys, with subtle change of semantics; tuned output;
2014-04-02 hoelzl 2014-04-02 extend continuous_intros; remove continuous_on_intros and isCont_intros
2014-04-02 hoelzl 2014-04-02 reorder Complex_Analysis_Basics; rename DD to deriv
2014-04-02 hoelzl 2014-04-02 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
2014-04-02 wenzelm 2014-04-02 merged;
2014-04-02 wenzelm 2014-04-02 tuned rendering;
2014-04-02 paulson 2014-04-02 new theorem about zero limits
2014-04-02 paulson 2014-04-02 New theorems for extracting quotients
2014-04-02 wenzelm 2014-04-02 more contributors;
2014-04-01 Andreas Lochbihler 2014-04-01 document value generation for quickcheck's testers
2014-04-02 wenzelm 2014-04-02 tuned whitespace;
2014-04-02 wenzelm 2014-04-02 suppress slightly odd completion of "simp";
2014-04-02 wenzelm 2014-04-02 observe extra line spacing for output as well;
2014-04-02 wenzelm 2014-04-02 persistent protocol_status, to improve performance of node_status a little;
2014-04-02 wenzelm 2014-04-02 more uniform painting of caret, which also improves visibility in invisible state;
2014-04-02 wenzelm 2014-04-02 tuned rendering -- visual indication of the status range, to make more clear when information might is out of view;