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;
Mon, 02 May 2011 01:05:50 +0200 wenzelm modernized rail diagrams using @{rail} antiquotation;
Mon, 02 May 2011 01:05:24 +0200 blanchet tuning
Mon, 02 May 2011 01:05:14 +0200 blanchet fixed parsing of multiple negations (e.g. ~~~p) found in Vampire proofs
Sun, 01 May 2011 22:36:58 +0200 blanchet use "metis", not "metisFT", to reconstruct proofs found in fully-typed mode -- "metisFT" is just too slow...
Sun, 01 May 2011 21:53:32 +0200 blanchet beware of polymorphic types in typed translation symbol declarations -- match alpha-equivalent types and, more importantly, prevent unsoundnesses by generating type constraints on the arguments of a polymorphic symbols (otherwise "hAPP" can be given any result type)
Sun, 01 May 2011 18:57:45 +0200 blanchet minor doc fixes
Sun, 01 May 2011 18:52:38 +0200 blanchet adapt to new type system names
Sun, 01 May 2011 18:37:25 +0200 blanchet restructured type systems some more -- the old naming schemes had "argshg diff |less" and "tagshg diff |less" as equivalent and didn't support a monomorphic version of "tags"
Sun, 01 May 2011 18:37:25 +0200 blanchet take "partial_types" option with a grain of salt
Sun, 01 May 2011 18:37:25 +0200 blanchet fixed SPASS fact offset calculation and report unexpected unsound proofs with so-called sound encodings
Sun, 01 May 2011 18:37:25 +0200 blanchet close formula universally, to make SPASS happy
Sun, 01 May 2011 18:37:25 +0200 blanchet fixed embarrassing bug where conjecture and fact offsets were swapped
Sun, 01 May 2011 18:37:25 +0200 blanchet pick up GaveUp error on SystemOnTPTP
Sun, 01 May 2011 18:37:25 +0200 blanchet avoid trailing digits for SNARK (type) names -- grr...
Sun, 01 May 2011 18:37:25 +0200 blanchet document new type system syntax
Sun, 01 May 2011 18:37:25 +0200 blanchet use ! for mildly unsound and !! for very unsound encodings
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip