Fri, 28 Oct 2005 22:27:54 +0200 wenzelm added add_local/add_global;
Fri, 28 Oct 2005 22:27:52 +0200 wenzelm added incr_indexes;
Fri, 28 Oct 2005 22:27:51 +0200 wenzelm renamed Goal constant to prop;
Fri, 28 Oct 2005 22:27:47 +0200 wenzelm accomodate simplified Thm.lift_rule;
Fri, 28 Oct 2005 22:27:46 +0200 wenzelm Logic.unprotect;
Fri, 28 Oct 2005 22:27:44 +0200 wenzelm literal facts;
Fri, 28 Oct 2005 22:27:41 +0200 wenzelm * Pure/Isar: literal facts;
Fri, 28 Oct 2005 22:26:10 +0200 wenzelm tuned;
Fri, 28 Oct 2005 20:18:37 +0200 webertj unnecessary imports removed
Fri, 28 Oct 2005 18:53:26 +0200 urbanc fixed case names in the weak induction principle and
Fri, 28 Oct 2005 18:22:26 +0200 berghofe Implemented proof of weak induction theorem.
Fri, 28 Oct 2005 17:59:07 +0200 berghofe Added "deepen" method.
Fri, 28 Oct 2005 17:27:49 +0200 haftmann circumvented smlnj value restriction
Fri, 28 Oct 2005 17:27:04 +0200 haftmann added extraction interface for code generator
Fri, 28 Oct 2005 16:43:46 +0200 urbanc Added (optional) arguments to the tactics
Fri, 28 Oct 2005 16:35:40 +0200 haftmann cleaned up nth, nth_update, nth_map and nth_string functions
Fri, 28 Oct 2005 13:52:57 +0200 berghofe Removed legacy prove_goalw_cterm command.
Fri, 28 Oct 2005 12:22:34 +0200 paulson got rid of obsolete prove_goalw_cterm
Fri, 28 Oct 2005 09:36:19 +0200 haftmann swapped add_datatype result
Fri, 28 Oct 2005 09:35:04 +0200 haftmann removed obfuscating PStrStrTab
Fri, 28 Oct 2005 08:40:55 +0200 haftmann reachable - abandoned foldl_map in favor of fold_map
Fri, 28 Oct 2005 02:30:53 +0200 mengj Added Tools/res_hol_clause.ML
Fri, 28 Oct 2005 02:30:12 +0200 mengj Added a new file res_hol_clause.ML to Reconstruction.thy. This file is used to translate HOL formulae into FOL clauses.
Fri, 28 Oct 2005 02:29:01 +0200 mengj Added "writeln_strs" to the signature
Fri, 28 Oct 2005 02:28:20 +0200 mengj Added several new functions that are used to prove HOL goals. Added new methods "vampireH" and "eproverH" that can prove both FOL and HOL goals. The old "vampire" and "eprover" methods are renamed to "vampireF" and "eproverF"; they can only prove FOL goals.
Fri, 28 Oct 2005 02:27:19 +0200 mengj Added new functions to handle HOL goals and lemmas.
Fri, 28 Oct 2005 02:25:57 +0200 mengj Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
Fri, 28 Oct 2005 02:24:58 +0200 mengj Added several functions to the signature.
Fri, 28 Oct 2005 02:23:49 +0200 mengj A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
Thu, 27 Oct 2005 18:25:33 +0200 paulson sorted lemma lists
Thu, 27 Oct 2005 13:59:06 +0200 wenzelm * HOL: alternative iff syntax;
Thu, 27 Oct 2005 13:54:43 +0200 wenzelm consts: monomorphic;
Thu, 27 Oct 2005 13:54:42 +0200 wenzelm removed inappropriate monomorphic test;
Thu, 27 Oct 2005 13:54:40 +0200 wenzelm replaced Defs.monomorphic by Sign.monomorphic;
Thu, 27 Oct 2005 13:54:38 +0200 wenzelm alternative iff syntax for equality on booleans, with print_mode 'iff';
Thu, 27 Oct 2005 08:14:05 +0200 haftmann added module Pure/General/rat.ML
Wed, 26 Oct 2005 16:31:53 +0200 paulson tidied away duplicate thm
Tue, 25 Oct 2005 18:38:21 +0200 wenzelm EVERY;
Tue, 25 Oct 2005 18:18:59 +0200 wenzelm traceIt: plain term;
Tue, 25 Oct 2005 18:18:58 +0200 wenzelm val legacy = ref false;
Tue, 25 Oct 2005 18:18:57 +0200 wenzelm prove_raw: cterms, explicit asms;
Tue, 25 Oct 2005 18:18:49 +0200 wenzelm avoid legacy goals;
Sat, 22 Oct 2005 01:22:10 +0200 wenzelm legacy = ref true for the time being -- avoid volumious warnings;
Fri, 21 Oct 2005 18:20:29 +0200 wenzelm tuned;
Fri, 21 Oct 2005 18:17:00 +0200 wenzelm avoid OldGoals shortcuts;
Fri, 21 Oct 2005 18:16:57 +0200 wenzelm * Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
Fri, 21 Oct 2005 18:15:00 +0200 wenzelm Internal goals.
Fri, 21 Oct 2005 18:14:59 +0200 wenzelm renamed triv_goal to goalI, rev_triv_goal to goalD;
Fri, 21 Oct 2005 18:14:58 +0200 wenzelm tuned header;
Fri, 21 Oct 2005 18:14:57 +0200 wenzelm Goal.norm_hhf_rule;
Fri, 21 Oct 2005 18:14:56 +0200 wenzelm export add_binds_i;
Fri, 21 Oct 2005 18:14:55 +0200 wenzelm load_file: setmp OldGoals.legacy true;
Fri, 21 Oct 2005 18:14:54 +0200 wenzelm improved check_result;
Fri, 21 Oct 2005 18:14:53 +0200 wenzelm Goal.prove_plain;
Fri, 21 Oct 2005 18:14:52 +0200 wenzelm do not export find_thms;
Fri, 21 Oct 2005 18:14:51 +0200 wenzelm use obsolete goals.ML here;
Fri, 21 Oct 2005 18:14:50 +0200 wenzelm Goal.conclude;
Fri, 21 Oct 2005 18:14:49 +0200 wenzelm moved SELECT_GOAL to goal.ML;
Fri, 21 Oct 2005 18:14:48 +0200 wenzelm moved norm_hhf_rule, prove etc. to goal.ML;
Fri, 21 Oct 2005 18:14:47 +0200 wenzelm added simplification tactics and rules (from meta_simplifier.ML);
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip