Sat, 31 Jul 2010 21:14:20 +0200 ballarin Make registrations generic data.
Fri, 30 Jul 2010 15:03:42 +0200 blanchet merged
Fri, 30 Jul 2010 00:02:25 +0200 blanchet don't choke on synonyms when parsing SPASS's Flotter output + renamings;
Thu, 29 Jul 2010 23:37:10 +0200 blanchet fix Mirabelle timeout
Thu, 29 Jul 2010 23:24:07 +0200 blanchet make Mirabelle happy
Thu, 29 Jul 2010 23:11:35 +0200 blanchet fix bug in the newly introduced "bound concealing" code
Thu, 29 Jul 2010 22:57:36 +0200 blanchet handle division by zero gracefully (used to raise Unordered later on)
Thu, 29 Jul 2010 22:43:46 +0200 blanchet use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
Thu, 29 Jul 2010 22:13:15 +0200 blanchet fix Meson's definition of first-orderness to prevent errors later on elsewhere (e.g. in Metis)
Thu, 29 Jul 2010 21:20:24 +0200 blanchet handle schematic vars the same way in Sledgehammer as in Metis, to avoid unreplayable proofs
Thu, 29 Jul 2010 20:15:50 +0200 blanchet revert exception throwing in FOL_SOLVE, since they're not caught anyway
Thu, 29 Jul 2010 20:02:02 +0200 blanchet avoid "ATP Error: Error: blah" style messages
Thu, 29 Jul 2010 19:58:43 +0200 blanchet avoid "_def_raw" theorems
Thu, 29 Jul 2010 19:26:42 +0200 blanchet better error and minimizer output
Thu, 29 Jul 2010 19:03:46 +0200 blanchet deal with chained facts more gracefully
Thu, 29 Jul 2010 18:45:41 +0200 blanchet speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
Thu, 29 Jul 2010 17:45:22 +0200 blanchet work around atomization failures
Thu, 29 Jul 2010 16:54:46 +0200 blanchet fiddle with the fudge factors, to get similar results as before
Thu, 29 Jul 2010 16:41:32 +0200 blanchet perform the presimplification done by Metis.make_nnf in Sledgehammer again, to deal with "If" and similar constructs
Thu, 29 Jul 2010 16:11:02 +0200 blanchet fix bug with "=" vs. "fequal" introduced by last change (dddb8ba3a1ce)
Thu, 29 Jul 2010 15:50:26 +0200 blanchet generate correct names for "$true" and "$false";
Thu, 29 Jul 2010 15:37:27 +0200 blanchet don't assume canonical rule format
Thu, 29 Jul 2010 14:53:55 +0200 blanchet avoid "clause" and "cnf" terminology where it no longer makes sense
Thu, 29 Jul 2010 14:42:09 +0200 blanchet "axiom_clauses" -> "axioms" (these are no longer clauses)
Thu, 29 Jul 2010 14:39:43 +0200 blanchet remove the "extra_clauses" business introduced in 19a5f1c8a844;
Thu, 29 Jul 2010 18:16:35 +0200 bulwahn adapting output for first solution
Thu, 29 Jul 2010 17:27:59 +0200 bulwahn removing pointless type information in internal prolog terms
Thu, 29 Jul 2010 17:27:58 +0200 bulwahn cleaning example file; more natural ordering of variable names
Thu, 29 Jul 2010 17:27:57 +0200 bulwahn improving translation to prolog; restoring terms from prolog output; adding tracing support
Thu, 29 Jul 2010 17:27:57 +0200 bulwahn working on parser for prolog reponse
Thu, 29 Jul 2010 17:27:56 +0200 bulwahn querying for multiple solutions in values command for prolog execution
Thu, 29 Jul 2010 17:27:55 +0200 bulwahn correcting scanning
Thu, 29 Jul 2010 17:27:55 +0200 bulwahn adding values command and parsing prolog output
Thu, 29 Jul 2010 17:27:54 +0200 bulwahn adding example file for prolog code generation; adding prolog code generation example to IsaMakefile
Thu, 29 Jul 2010 17:27:52 +0200 bulwahn adding a mockup version for prolog code generation
Thu, 29 Jul 2010 17:27:51 +0200 bulwahn exporting retrieval function for graph of introduction rules in the predicate compiler core
Thu, 29 Jul 2010 15:07:52 +0200 haftmann merged
Thu, 29 Jul 2010 12:28:45 +0200 haftmann rebinding ref is illegal
Thu, 29 Jul 2010 12:28:45 +0200 haftmann tuned example
Thu, 29 Jul 2010 12:28:45 +0200 haftmann intermediate operation avoids invariance problem in Scala
Thu, 29 Jul 2010 12:07:09 +0200 blanchet merged
Thu, 29 Jul 2010 09:47:23 +0200 blanchet kill polymorphic "val"s
Thu, 29 Jul 2010 09:41:49 +0200 blanchet improved ATP error handling some more
Thu, 29 Jul 2010 00:28:57 +0200 blanchet shorter URL
Wed, 28 Jul 2010 23:44:18 +0200 blanchet mention version numbers
Wed, 28 Jul 2010 23:05:35 +0200 blanchet fiddled with usage text
Wed, 28 Jul 2010 23:01:27 +0200 blanchet handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
Thu, 29 Jul 2010 09:57:10 +0200 haftmann merged
Thu, 29 Jul 2010 09:57:00 +0200 haftmann tuned printing of applications and let cascades
Thu, 29 Jul 2010 09:56:59 +0200 haftmann checking Scala_imp
Thu, 29 Jul 2010 09:56:59 +0200 haftmann proper unit type in transformed program
Thu, 29 Jul 2010 08:16:49 +0200 haftmann merged
Wed, 28 Jul 2010 14:11:48 +0200 haftmann merged
Wed, 28 Jul 2010 12:12:32 +0200 haftmann tuned; added pretty numerals for code generation
Wed, 28 Jul 2010 12:12:29 +0200 haftmann may use `int` in Isabelle runtime environment
Wed, 28 Jul 2010 14:09:56 +0200 haftmann dropped dead code
Wed, 28 Jul 2010 22:18:35 +0200 blanchet merged
Wed, 28 Jul 2010 19:42:11 +0200 blanchet make Mirabelle happy
Wed, 28 Jul 2010 19:23:56 +0200 blanchet renamed environment variable
Wed, 28 Jul 2010 19:07:34 +0200 blanchet updated component name
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip