Tue, 03 May 2011 16:54:26 +0200 wenzelm sane paragraph layout;
Tue, 03 May 2011 16:00:29 +0200 wenzelm updated configuration options -- no ML here;
Tue, 03 May 2011 15:37:17 +0200 wenzelm tag ML as in IsarImplementation;
Tue, 03 May 2011 15:35:07 +0200 wenzelm treat underscore as in IsarRef;
Tue, 03 May 2011 15:29:49 +0200 wenzelm reactivated codegen example based on Lambda.thy;
Tue, 03 May 2011 15:07:36 +0200 wenzelm formal Base theory;
Tue, 03 May 2011 14:23:40 +0200 blanchet reintroduce this idea of running "metisFT" after a failed "metis" -- I took it out in e85ce10cef1a because I couldn't think of a reasonable use case, but now that ATPs use sound encodings and include dangerous facts (e.g. True_or_False) it makes more sense than ever to run "metisFT" after "metis"
Tue, 03 May 2011 08:52:32 +0200 blanchet whitespace tuning
Tue, 03 May 2011 08:52:16 +0200 blanchet make SML/NJ happiest
Tue, 03 May 2011 01:04:03 +0200 blanchet no need to generate fact numbers for polymorphic type systems -- this confuses the TPTP exporter
Tue, 03 May 2011 00:10:22 +0200 blanchet replaced some Unsynchronized.refs with Config.Ts
Mon, 02 May 2011 23:01:22 +0200 blanchet do not declare TPTP built-ins, e.g. $true
Mon, 02 May 2011 22:52:15 +0200 blanchet SNARK workaround
Mon, 02 May 2011 22:52:15 +0200 blanchet better default type systems for SNARK and ToFoF
Mon, 02 May 2011 22:52:15 +0200 blanchet tuning
Mon, 02 May 2011 22:52:15 +0200 blanchet recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
Mon, 02 May 2011 22:52:15 +0200 blanchet generate tags for simps, intros, and elims in TPTP poblems on demand
Mon, 02 May 2011 22:52:15 +0200 blanchet proper default for TPTP source filed
Mon, 02 May 2011 22:52:15 +0200 blanchet have each ATP filter out dangerous facts for themselves, based on their type system
Mon, 02 May 2011 22:31:46 +0200 wenzelm eliminated old CVS Ids;
Mon, 02 May 2011 22:19:28 +0200 wenzelm no use of package rail;
Mon, 02 May 2011 22:06:49 +0200 wenzelm obsolete;
Mon, 02 May 2011 22:05:47 +0200 wenzelm removed rail garbage;
Mon, 02 May 2011 22:03:18 +0200 wenzelm NEWS;
Mon, 02 May 2011 22:00:38 +0200 wenzelm just one railsetup.sty which is shipped with the official distribution to accompany @{rail} in Pure;
Mon, 02 May 2011 21:59:47 +0200 wenzelm proper treatment of underscore in rail diagrams;
Mon, 02 May 2011 21:46:54 +0200 wenzelm simplified rail setup, using plain defaults (NB: \small is incompatible with \isabellestyle used here);
Mon, 02 May 2011 21:42:36 +0200 wenzelm eliminated external rail executable;
Mon, 02 May 2011 21:41:39 +0200 wenzelm removed obsolete rail diagrams (which were about old-style theory syntax);
Mon, 02 May 2011 21:33:21 +0200 wenzelm moved material about old codegen to isar-ref manual;
Mon, 02 May 2011 20:34:34 +0200 wenzelm eliminated some duplicate "def" positions;
Mon, 02 May 2011 20:14:19 +0200 wenzelm 'axiomatization' is global;
Mon, 02 May 2011 19:55:24 +0200 wenzelm discontinued old version of old HOL manual;
Mon, 02 May 2011 17:43:42 +0200 wenzelm merged
Mon, 02 May 2011 17:43:06 +0200 wenzelm removed obsolete rail setup;
Mon, 02 May 2011 17:28:45 +0200 wenzelm uniform content markup;
Mon, 02 May 2011 17:28:09 +0200 wenzelm eliminated obsolete rail macros;
Mon, 02 May 2011 17:12:11 +0200 wenzelm removed obsolete rail diagram (which was about old-style theory syntax);
Mon, 02 May 2011 17:07:46 +0200 wenzelm eliminated separate rail/latex phase;
Mon, 02 May 2011 17:06:40 +0200 wenzelm more precise rail diagrams;
Mon, 02 May 2011 16:33:21 +0200 wenzelm added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
Mon, 02 May 2011 15:13:10 +0200 blanchet make SML/NJ happier
Mon, 02 May 2011 15:01:36 +0200 blanchet make "debug" more verbose and "verbose" less verbose
Mon, 02 May 2011 14:40:57 +0200 blanchet use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
Mon, 02 May 2011 14:28:28 +0200 blanchet cosmetics
Mon, 02 May 2011 14:22:34 +0200 blanchet supply type-system defaults for major ATPs
Mon, 02 May 2011 14:21:57 +0200 blanchet make sure that "file" annotations are read correctly in SInE-E and E proofs
Mon, 02 May 2011 14:10:09 +0200 blanchet fixed random number invocation
Mon, 02 May 2011 13:52:15 +0200 blanchet make sure E type information constants are given a weight, even if they don't appear anywhere else
Mon, 02 May 2011 13:29:47 +0200 blanchet fix ROOT.ML and handle "readable_names" reference slightly more cleanly
Mon, 02 May 2011 12:09:33 +0200 blanchet show sorts not just types in Isar proofs + tuning
Mon, 02 May 2011 12:09:33 +0200 blanchet Vampire sometimes generates formulas with ~ (not) followed by a quantified subformula, without parentheses -- parse these correctly
Mon, 02 May 2011 12:09:33 +0200 blanchet tuning
Mon, 02 May 2011 12:09:33 +0200 blanchet make SML/NJ happy
Mon, 02 May 2011 12:09:33 +0200 blanchet added TPTP exporter facility -- useful to do experiments with machine learning
Mon, 02 May 2011 12:09:33 +0200 blanchet renamed theory to make its purpose clearer
Mon, 02 May 2011 10:50:09 +0200 bulwahn fixing typo
Mon, 02 May 2011 10:50:09 +0200 bulwahn improving naming of fresh variables in OCaml serializer
Mon, 02 May 2011 10:50:07 +0200 bulwahn adding code generation setup for String.implode and String.explode in OCaml (contributed by Andreas Lochbihler)
Mon, 02 May 2011 01:20:28 +0200 wenzelm merged;
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip