2011-05-26 hoelzl 2011-05-26 add lemma kolmogorov_0_1_law
2011-05-26 hoelzl 2011-05-26 add lemma indep_sets_collect_sigma
2011-05-26 bulwahn 2011-05-26 improving code_int setup in Quickcheck_Narrowing; adding partial_term_of class in Quickcheck_Narrowing
2011-05-26 bulwahn 2011-05-26 extending terms of Code_Evaluation by Free to allow partial terms
2011-05-26 krauss 2011-05-26 adhoc event handler to insert 'sendback' text into the buffer, replacing the original command
2011-05-26 krauss 2011-05-26 css rules for highlighting sendback text
2011-05-26 krauss 2011-05-26 invert event propagation flag -- in lobobrowser api, true means re-propagate
2011-05-25 blanchet 2011-05-25 eta-expand to make SML/NJ happy
2011-05-24 blanchet 2011-05-24 ensure that the argument of logical negation is enclosed in parentheses in THF mode
2011-05-24 blanchet 2011-05-24 hack to obtain potable step names from Waldmeister
2011-05-24 blanchet 2011-05-24 respect user's intention better when setting the CNF_UEQ type system (esp. w.r.t. "erased")
2011-05-24 blanchet 2011-05-24 further reduce the number of facts passed to less used remote ATPs
2011-05-24 blanchet 2011-05-24 added quietness flag
2011-05-24 blanchet 2011-05-24 pass fewer relevant facts to less used remote systems
2011-05-24 blanchet 2011-05-24 more work on parsing LEO-II proofs and extracting uses of extensionality
2011-05-24 blanchet 2011-05-24 tuning
2011-05-24 blanchet 2011-05-24 more work on parsing LEO-II proofs without lambdas
2011-05-24 blanchet 2011-05-24 slightly gracefuller handling of LEO-II and Satallax output
2011-05-24 blanchet 2011-05-24 document primitive support for LEO-II and Satallax
2011-05-24 blanchet 2011-05-24 identify HOL functions with THF functions
2011-05-24 blanchet 2011-05-24 started adding support for THF output (but no lambdas)
2011-05-24 blanchet 2011-05-24 eliminated more code duplication in Nitrox
2011-05-24 blanchet 2011-05-24 reduce code duplication in Nitrox
2011-05-24 blanchet 2011-05-24 use \<emdash> rather than \<midarrow>
2011-05-24 blanchet 2011-05-24 fixed de Bruijn index bug
2011-05-24 blanchet 2011-05-24 use "eq_thm_prop" for slacker comparison -- ensures that backtick-quoted chained facts are recognized in the minimizer, among other things
2011-05-24 blanchet 2011-05-24 filter Waldmeister facts better -- and don't encode type classes as predicates, since it doesn't like conditional equations
2011-05-24 blanchet 2011-05-24 clearer SystemOnTPTP errors
2011-05-24 blanchet 2011-05-24 give fewer equations to Waldmeister
2011-05-24 blanchet 2011-05-24 detect inappropriate problems and crashes better in Waldmeister
2011-05-24 blanchet 2011-05-24 tuning -- the "appropriate" terminology is inspired from TPTP
2011-05-24 blanchet 2011-05-24 pass no type args to hAPP in "poly_args" type system, which is unsound anyway and should correspond as closely as possible to the old unsound encoding
2011-05-23 hoelzl 2011-05-23 move lemmas to Extended_Reals and Extended_Real_Limits
2011-05-23 krauss 2011-05-23 separate initializations for different modes of partial_function -- generation of induction rules will be non-uniform
2011-05-22 krauss 2011-05-22 reverted 7fdd8d4908dc -- keeping images from Isabelle_makeall would be too expensive
2011-05-22 krauss 2011-05-22 fun command produces warning when patterns are incomplete (somewhat analogous to primrec)
2011-05-22 blanchet 2011-05-22 added message when Waldmeister isn't run
2011-05-22 blanchet 2011-05-22 slightly improved documentation
2011-05-22 blanchet 2011-05-22 improved Waldmeister support -- even run it by default on unit equational goals
2011-05-22 blanchet 2011-05-22 fish out axioms in Waldmeister output
2011-05-22 blanchet 2011-05-22 removed SNARK hack now that SNARK is fixed
2011-05-22 blanchet 2011-05-22 recognize one more SystemOnTPTP error
2011-05-22 blanchet 2011-05-22 document Waldmeister
2011-05-22 blanchet 2011-05-22 added support for remote Waldmeister
2011-05-22 blanchet 2011-05-22 added Waldmeister
2011-05-22 blanchet 2011-05-22 reorganized ATP formats a little bit
2011-06-06 wenzelm 2011-06-06 tuned;
2011-06-06 wenzelm 2011-06-06 removed odd remains of low-level session management;
2011-06-06 wenzelm 2011-06-06 moved incr_boundvars; discontinued low-level term operations;
2011-06-06 wenzelm 2011-06-06 modernized and re-unified Thm.transfer;
2011-06-06 wenzelm 2011-06-06 removed obsolete material (superseded by implementation manual);
2011-06-05 wenzelm 2011-06-05 removed somewhat low-level stuff (cf. attribute "swapped" in isar-ref);
2011-06-05 wenzelm 2011-06-05 updated and re-unified classical proof methods; tuned;
2011-06-05 wenzelm 2011-06-05 tuned;
2011-06-05 wenzelm 2011-06-05 updated and re-unified classical rule declarations;
2011-06-04 wenzelm 2011-06-04 moved/updated introduction to Classical Reasoner;
2011-06-04 wenzelm 2011-06-04 tuned secref (still dangling);
2011-06-03 wenzelm 2011-06-03 updated and re-unified material on simprocs;
2011-06-03 wenzelm 2011-06-03 removed some old stuff;
2011-06-02 wenzelm 2011-06-02 tuned headings;