2011-07-27 hoelzl 2011-07-27 to_nat is injective on arbitrary domains
2011-07-27 hoelzl 2011-07-27 finite vimage on arbitrary domains
2011-07-26 blanchet 2011-07-26 updated Sledgehammer documentation
2011-07-26 blanchet 2011-07-26 renamed "preds" encodings to "guards"
2011-07-26 bulwahn 2011-07-26 more precise dependencies
2011-07-26 blanchet 2011-07-26 further worked around LEO-II parser limitation, with eta-expansion
2011-07-26 blanchet 2011-07-26 use syntactic sugar whenever possible in THF problems, to work around current LEO-II parser limitation (bang bang and query query are not handled correctly)
2011-07-26 blanchet 2011-07-26 no need for existential witnesses for sorts in TFF and THF formats
2011-07-26 blanchet 2011-07-26 mangle "undefined"
2011-07-26 blanchet 2011-07-26 tuning -- remove useless function (at this point combinators are already in)
2011-07-26 blanchet 2011-07-26 remove spurious message
2011-07-26 blanchet 2011-07-26 give E at least two seconds -- anything else risks causing too early timeouts in the minimizer, because of too conservative time computations in E and eproof scripts
2011-07-26 Andreas Lochbihler 2011-07-26 merged
2011-07-26 Andreas Lochbihler 2011-07-26 fixed code generator setup in List_Cset
2011-07-26 hoelzl 2011-07-26 enat is a complete_linorder instance
2011-07-26 Andreas Lochbihler 2011-07-26 merged
2011-07-26 Andreas Lochbihler 2011-07-26 Add theory for setting up monad syntax for Cset
2011-07-26 bulwahn 2011-07-26 merged
2011-07-26 bulwahn 2011-07-26 removing expectations from quickcheck example
2011-07-26 bulwahn 2011-07-26 adding remarks after static inspection of the invocation of the SML code generator
2011-07-26 Andreas Lochbihler 2011-07-26 merged
2011-07-25 Andreas Lochbihler 2011-07-25 added operations to Cset with code equations in backing implementations
2011-07-25 haftmann 2011-07-25 merged
2011-07-25 haftmann 2011-07-25 adjusted to tailored version of ball_simps
2011-07-24 haftmann 2011-07-24 adjusted to tailored version of bex_simps
2011-07-24 haftmann 2011-07-24 more coherent structure in and across theories
2011-07-25 blanchet 2011-07-25 declare "undefined" constant
2011-07-25 blanchet 2011-07-25 make compile
2011-07-25 blanchet 2011-07-25 thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
2011-07-25 blanchet 2011-07-25 tuning
2011-07-25 blanchet 2011-07-25 introduced hybrid lambda translation
2011-07-25 blanchet 2011-07-25 avoid needless type args for lifted-lambdas
2011-07-25 bulwahn 2011-07-25 replacing conversion function of old code generator by the current code generator in the reflection tactic
2011-07-25 bulwahn 2011-07-25 fixed typo
2011-07-25 bulwahn 2011-07-25 removing SML_Quickcheck
2011-07-25 bulwahn 2011-07-25 NEWS
2011-07-25 bulwahn 2011-07-25 added legacy warning to old code generation evaluation
2011-07-25 bulwahn 2011-07-25 added legacy warning to old code generation commands
2011-07-23 wenzelm 2011-07-23 merged
2011-07-23 bulwahn 2011-07-23 correcting last example in Predicate_Compile_Examples
2011-07-23 wenzelm 2011-07-23 make double-sure that interrupts are flushed before executing new work (cf. 22f8c2483bd2);
2011-07-23 wenzelm 2011-07-23 more detailed tracing; tuned;
2011-07-23 wenzelm 2011-07-23 defensive Term_Sharing, to avoid extending trusted code base of inference kernel;
2011-07-23 wenzelm 2011-07-23 more precise parse_name according to XML standard; tuned performance;
2011-07-23 wenzelm 2011-07-23 explicit structure ML_System; tunned ML bootstrap;
2011-07-23 wenzelm 2011-07-23 defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
2011-07-23 wenzelm 2011-07-23 tuned;
2011-07-22 haftmann 2011-07-22 merged
2011-07-22 haftmann 2011-07-22 dropped errorneous hint
2011-07-21 haftmann 2011-07-21 moved some lemmas
2011-07-21 haftmann 2011-07-21 merged
2011-07-21 haftmann 2011-07-21 ereal is a complete_linorder instance
2011-07-20 haftmann 2011-07-20 class complete_linorder
2011-07-21 blanchet 2011-07-21 make "concealed" lambda translation sound
2011-07-21 bulwahn 2011-07-21 deactivating all quickcheck invocations until parallel invocation works safely
2011-07-21 bulwahn 2011-07-21 adapting two examples in Predicate_Compile_Examples
2011-07-20 blanchet 2011-07-20 use a more robust naming convention for "polymorphic" frees -- the check is an overapproximation but that's fine as far as soundness is concerned
2011-07-20 Cezary Kaliszyk 2011-07-20 merge
2011-07-20 Cezary Kaliszyk 2011-07-20 Quotient Package: handle Bound variables in rep_abs_rsp_tac not only at top-level of the goal
2011-07-20 hoelzl 2011-07-20 add code generator setup and tests for ereal