Fri, 28 Oct 2005 22:32:55 +0200 wenzelm lthms_containing: not o valid_thms;
Fri, 28 Oct 2005 22:28:15 +0200 wenzelm added fact_tac, some_fact_tac;
Fri, 28 Oct 2005 22:28:13 +0200 wenzelm renamed Goal constant to prop, more general protect/unprotect interfaces;
Fri, 28 Oct 2005 22:28:12 +0200 wenzelm renamed Goal constant to prop, more general protect/unprotect interfaces;
Fri, 28 Oct 2005 22:28:11 +0200 wenzelm added fact method;
Fri, 28 Oct 2005 22:28:09 +0200 wenzelm tuned ProofContext.export interfaces;
Fri, 28 Oct 2005 22:28:07 +0200 wenzelm syntax for literal facts;
Fri, 28 Oct 2005 22:28:06 +0200 wenzelm removed try_dest_Goal, use Logic.unprotect;
Fri, 28 Oct 2005 22:28:04 +0200 wenzelm added cgoal_of;
Fri, 28 Oct 2005 22:28:03 +0200 wenzelm accomodate simplified Thm.lift_rule;
Fri, 28 Oct 2005 22:28:02 +0200 wenzelm export cong_modifiers, simp_modifiers';
Fri, 28 Oct 2005 22:28:00 +0200 wenzelm certify_term: tuned monomorphic consts;
Fri, 28 Oct 2005 22:27:59 +0200 wenzelm datatype thmref: added Fact;
Fri, 28 Oct 2005 22:27:58 +0200 wenzelm Logic.lift_all;
Fri, 28 Oct 2005 22:27:57 +0200 wenzelm renamed Goal constant to prop, more general protect/unprotect interfaces;
Fri, 28 Oct 2005 22:27:56 +0200 wenzelm renamed Goal.norm_hhf_rule to Goal.norm_hhf;
Fri, 28 Oct 2005 22:27:55 +0200 wenzelm renamed Goal constant to prop, more general protect/unprotect interfaces;
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;
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip