Wed, 27 Jul 2011 19:35:00 +0200 hoelzl to_nat is injective on arbitrary domains
Wed, 27 Jul 2011 19:34:30 +0200 hoelzl finite vimage on arbitrary domains
Tue, 26 Jul 2011 22:53:06 +0200 blanchet updated Sledgehammer documentation
Tue, 26 Jul 2011 22:53:06 +0200 blanchet renamed "preds" encodings to "guards"
Tue, 26 Jul 2011 18:11:38 +0200 bulwahn more precise dependencies
Tue, 26 Jul 2011 14:53:00 +0200 blanchet further worked around LEO-II parser limitation, with eta-expansion
Tue, 26 Jul 2011 14:53:00 +0200 blanchet 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)
Tue, 26 Jul 2011 14:53:00 +0200 blanchet no need for existential witnesses for sorts in TFF and THF formats
Tue, 26 Jul 2011 14:53:00 +0200 blanchet mangle "undefined"
Tue, 26 Jul 2011 14:53:00 +0200 blanchet tuning -- remove useless function (at this point combinators are already in)
Tue, 26 Jul 2011 14:53:00 +0200 blanchet remove spurious message
Tue, 26 Jul 2011 14:53:00 +0200 blanchet 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
Tue, 26 Jul 2011 14:50:15 +0200 Andreas Lochbihler merged
Tue, 26 Jul 2011 14:05:28 +0200 Andreas Lochbihler fixed code generator setup in List_Cset
Tue, 26 Jul 2011 13:50:03 +0200 hoelzl enat is a complete_linorder instance
Tue, 26 Jul 2011 12:44:36 +0200 Andreas Lochbihler merged
Tue, 26 Jul 2011 10:49:34 +0200 Andreas Lochbihler Add theory for setting up monad syntax for Cset
Tue, 26 Jul 2011 11:48:11 +0200 bulwahn merged
Tue, 26 Jul 2011 08:07:01 +0200 bulwahn removing expectations from quickcheck example
Tue, 26 Jul 2011 08:07:00 +0200 bulwahn adding remarks after static inspection of the invocation of the SML code generator
Tue, 26 Jul 2011 10:03:19 +0200 Andreas Lochbihler merged
Mon, 25 Jul 2011 16:55:48 +0200 Andreas Lochbihler added operations to Cset with code equations in backing implementations
Mon, 25 Jul 2011 23:27:20 +0200 haftmann merged
Mon, 25 Jul 2011 23:26:55 +0200 haftmann adjusted to tailored version of ball_simps
Sun, 24 Jul 2011 22:38:13 +0200 haftmann adjusted to tailored version of bex_simps
Sun, 24 Jul 2011 21:27:25 +0200 haftmann more coherent structure in and across theories
Mon, 25 Jul 2011 14:10:12 +0200 blanchet declare "undefined" constant
Mon, 25 Jul 2011 14:10:12 +0200 blanchet make compile
Mon, 25 Jul 2011 14:10:12 +0200 blanchet thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
Mon, 25 Jul 2011 14:10:12 +0200 blanchet tuning
Mon, 25 Jul 2011 14:10:12 +0200 blanchet introduced hybrid lambda translation
Mon, 25 Jul 2011 14:10:12 +0200 blanchet avoid needless type args for lifted-lambdas
Mon, 25 Jul 2011 11:21:45 +0200 bulwahn replacing conversion function of old code generator by the current code generator in the reflection tactic
Mon, 25 Jul 2011 11:21:44 +0200 bulwahn fixed typo
Mon, 25 Jul 2011 10:43:14 +0200 bulwahn removing SML_Quickcheck
Mon, 25 Jul 2011 10:42:32 +0200 bulwahn NEWS
Mon, 25 Jul 2011 10:40:52 +0200 bulwahn added legacy warning to old code generation evaluation
Mon, 25 Jul 2011 10:40:51 +0200 bulwahn added legacy warning to old code generation commands
Sat, 23 Jul 2011 23:33:59 +0200 wenzelm merged
Sat, 23 Jul 2011 20:05:28 +0200 bulwahn correcting last example in Predicate_Compile_Examples
Sat, 23 Jul 2011 22:22:21 +0200 wenzelm make double-sure that interrupts are flushed before executing new work (cf. 22f8c2483bd2);
Sat, 23 Jul 2011 21:29:56 +0200 wenzelm more detailed tracing;
Sat, 23 Jul 2011 20:34:33 +0200 wenzelm defensive Term_Sharing, to avoid extending trusted code base of inference kernel;
Sat, 23 Jul 2011 20:11:18 +0200 wenzelm more precise parse_name according to XML standard;
Sat, 23 Jul 2011 17:22:28 +0200 wenzelm explicit structure ML_System;
Sat, 23 Jul 2011 16:37:17 +0200 wenzelm defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
Sat, 23 Jul 2011 16:12:12 +0200 wenzelm tuned;
Fri, 22 Jul 2011 07:33:34 +0200 haftmann merged
Fri, 22 Jul 2011 07:33:29 +0200 haftmann dropped errorneous hint
Thu, 21 Jul 2011 22:47:13 +0200 haftmann moved some lemmas
Thu, 21 Jul 2011 21:56:24 +0200 haftmann merged
Thu, 21 Jul 2011 18:40:31 +0200 haftmann ereal is a complete_linorder instance
Wed, 20 Jul 2011 22:14:39 +0200 haftmann class complete_linorder
Thu, 21 Jul 2011 21:29:10 +0200 blanchet make "concealed" lambda translation sound
Thu, 21 Jul 2011 08:33:57 +0200 bulwahn deactivating all quickcheck invocations until parallel invocation works safely
Thu, 21 Jul 2011 08:31:35 +0200 bulwahn adapting two examples in Predicate_Compile_Examples
Wed, 20 Jul 2011 23:47:27 +0200 blanchet use a more robust naming convention for "polymorphic" frees -- the check is an overapproximation but that's fine as far as soundness is concerned
Wed, 20 Jul 2011 16:15:33 +0200 Cezary Kaliszyk merge
Wed, 20 Jul 2011 16:14:49 +0200 Cezary Kaliszyk Quotient Package: handle Bound variables in rep_abs_rsp_tac not only at top-level of the goal
Wed, 20 Jul 2011 15:42:23 +0200 hoelzl add code generator setup and tests for ereal
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip