Sun, 01 May 2011 18:37:24 +0200 blanchet generate typing for "hBOOL" in "Many_Typed" mode + tuning
Sun, 01 May 2011 18:37:24 +0200 blanchet generate pure TFF problems -- ToFoF doesn't like mixtures of FOF and TFF, even when the two logics coincide (e.g. for ground formulas)
Sun, 01 May 2011 18:37:24 +0200 blanchet improve version handling -- prefer versions of ToFoF, SInE, and SNARK that are known to work
Sun, 01 May 2011 18:37:24 +0200 blanchet unprefix evil "fof_" prefix inserted by ToFoF
Sun, 01 May 2011 18:37:24 +0200 blanchet added support for ToFoF prover for experimenting with the TPTP TFF (typed first-order) format
Sun, 01 May 2011 18:37:24 +0200 blanchet fake type declarations for full-type args and mangled type encodings, so that type assumptions can be discharged
Sun, 01 May 2011 18:37:24 +0200 blanchet generate TFF type declarations in typed mode
Sun, 01 May 2011 18:37:24 +0200 blanchet no point in keeping indices in Sledgehammer readable var names, since these are disambiguated anyway
Sun, 01 May 2011 18:37:24 +0200 blanchet added more rudimentary type support to Sledgehammer's ATP encoding
Sun, 01 May 2011 18:37:24 +0200 blanchet fixed type of ATP quantifier types (sic)
Sun, 01 May 2011 18:37:24 +0200 blanchet added "useful_info" argument to ATP formulas -- this will probably be useful later to specify intro, simp, elim to SPASS
Sun, 01 May 2011 18:37:24 +0200 blanchet added support for TFF type declarations
Sun, 01 May 2011 18:37:24 +0200 blanchet reintroduced constructor for formulas, and automatically detect which logic to use (TFF or FOF) to avoid clutter
Sun, 01 May 2011 18:37:24 +0200 blanchet added room for types in ATP quantifiers
Sun, 01 May 2011 18:37:24 +0200 blanchet distinguish FOF and TFF (typed first-order) in ATP abstract syntax tree
Sun, 01 May 2011 18:37:24 +0200 blanchet remove experimental feature ("risky overload")
Sun, 01 May 2011 18:37:24 +0200 blanchet added (without implementation yet) new type encodings for Sledgehammer/ATP
Sun, 01 May 2011 18:37:23 +0200 blanchet close ATP formulas universally earlier, so that we can add type predicates
Sun, 01 May 2011 18:37:23 +0200 blanchet get rid of "explicit_forall" prover-specific option, even if that means some clutter -- foralls will be necessary to attach types to variables
Sun, 01 May 2011 18:37:23 +0200 blanchet renamings
Sun, 01 May 2011 18:05:09 +0200 wenzelm tuned;
Sun, 01 May 2011 17:55:29 +0200 wenzelm include static rail files for old manuals, to make standard make job independent of the "rail" executable;
Sun, 01 May 2011 17:42:21 +0200 wenzelm simplified keyword markup (without formal checking);
Sun, 01 May 2011 17:41:49 +0200 wenzelm treat @ as separate keyword;
Sun, 01 May 2011 17:19:46 +0200 wenzelm default rail fonts via isabellestyle;
Sun, 01 May 2011 17:13:44 +0200 wenzelm localized \isabellestyle;
Sun, 01 May 2011 16:56:50 +0200 wenzelm misc cleanup;
Sun, 01 May 2011 16:52:29 +0200 wenzelm misc cleanup -- no need to copy style files;
Sun, 01 May 2011 16:36:34 +0200 wenzelm eliminated copies of isabelle style files;
Sun, 01 May 2011 00:01:59 +0200 wenzelm use @{rail} antiquotation (with some nested markup);
Sat, 30 Apr 2011 23:27:57 +0200 wenzelm updated Variable.focus;
Sat, 30 Apr 2011 23:20:50 +0200 wenzelm allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
Sat, 30 Apr 2011 20:58:36 +0200 wenzelm tuned;
Sat, 30 Apr 2011 20:48:29 +0200 wenzelm more robust error handling (NB: Source.source requires total scanner or recover);
Sat, 30 Apr 2011 20:07:31 +0200 wenzelm removed old rail.ML;
Sat, 30 Apr 2011 19:50:39 +0200 wenzelm railroad diagrams in LaTeX as document antiquotation;
Sat, 30 Apr 2011 18:16:40 +0200 wenzelm more uniform variations of scan_string;
Thu, 28 Apr 2011 21:06:04 +0200 wenzelm literal facts `prop` may contain dummy patterns;
Thu, 28 Apr 2011 20:20:49 +0200 wenzelm eliminated slightly odd Proof_Context.bind_fixes;
Thu, 28 Apr 2011 09:32:28 +0200 berghofe merged
Wed, 27 Apr 2011 19:27:06 +0200 berghofe Properly treat proof functions with no arguments.
Wed, 27 Apr 2011 23:04:28 +0200 wenzelm merged
Wed, 27 Apr 2011 21:17:47 +0200 krauss inlined Function_Lib.replace_frees, which is used only once
Wed, 27 Apr 2011 23:02:43 +0200 wenzelm more precise positions via binding;
Wed, 27 Apr 2011 21:50:04 +0200 wenzelm clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;
Wed, 27 Apr 2011 20:58:40 +0200 wenzelm tuned signature -- eliminated odd comment;
Wed, 27 Apr 2011 20:37:56 +0200 wenzelm more informative markup for fixed variables (via name space entry);
Wed, 27 Apr 2011 20:28:27 +0200 wenzelm discontinued obsolete markup;
Wed, 27 Apr 2011 20:19:05 +0200 wenzelm more precise position information via Variable.add_fixes_binding;
Wed, 27 Apr 2011 19:55:42 +0200 wenzelm more formal treatment of parameters, avoiding slightly odd Variable.intern_fixed;
Wed, 27 Apr 2011 19:39:50 +0200 wenzelm some adhoc renaming, to accomodate more strict checks of fixes (cf. 4638622bcaa1);
Wed, 27 Apr 2011 17:58:45 +0200 wenzelm reorganized fixes as specialized (global) name space;
Wed, 27 Apr 2011 17:44:06 +0200 wenzelm export Name_Space.entry_ord;
Wed, 27 Apr 2011 17:20:29 +0200 wenzelm direct use of Variable.is_fixed;
Wed, 27 Apr 2011 14:11:37 +0200 wenzelm tuned;
Wed, 27 Apr 2011 13:21:12 +0200 wenzelm predefined LaTeX macros for \<bind> and \<then>;
Wed, 27 Apr 2011 10:49:39 +0200 wenzelm eliminated obsolete Function_Lib.frees_in_term;
Wed, 27 Apr 2011 10:31:18 +0200 wenzelm more uniform Variable.add_frees/add_fixed etc.;
Tue, 26 Apr 2011 22:22:39 +0200 wenzelm structure Cla as defined in FOL;
Tue, 26 Apr 2011 22:18:07 +0200 wenzelm proper antiquotations;
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip