wenzelm [Fri, 28 Oct 2005 22:27:58 +0200] rev 18030
Logic.lift_all;
wenzelm [Fri, 28 Oct 2005 22:27:57 +0200] rev 18029
renamed Goal constant to prop, more general protect/unprotect interfaces;
replaced lift_fns by lift_abs, lift_all;
wenzelm [Fri, 28 Oct 2005 22:27:56 +0200] rev 18028
renamed Goal.norm_hhf_rule to Goal.norm_hhf;
wenzelm [Fri, 28 Oct 2005 22:27:55 +0200] rev 18027
renamed Goal constant to prop, more general protect/unprotect interfaces;
renamed norm_hhf_rule to norm_hhf;
added comp_hhf, compose_hhf_tac, based on Drule.lift_all;
wenzelm [Fri, 28 Oct 2005 22:27:54 +0200] rev 18026
added add_local/add_global;
index props (for add_local only);
added could_unify;
wenzelm [Fri, 28 Oct 2005 22:27:52 +0200] rev 18025
added incr_indexes;
added lift_all (approx. reverse of gen_all);
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm [Fri, 28 Oct 2005 22:27:51 +0200] rev 18024
renamed Goal constant to prop;
wenzelm [Fri, 28 Oct 2005 22:27:47 +0200] rev 18023
accomodate simplified Thm.lift_rule;
wenzelm [Fri, 28 Oct 2005 22:27:46 +0200] rev 18022
Logic.unprotect;
wenzelm [Fri, 28 Oct 2005 22:27:44 +0200] rev 18021
literal facts;
wenzelm [Fri, 28 Oct 2005 22:27:41 +0200] rev 18020
* Pure/Isar: literal facts;
* ML/Pure: tuned Thm.lift_rule;
* ML/Pure: renamed Goal constant to prop, more general uses;
wenzelm [Fri, 28 Oct 2005 22:26:10 +0200] rev 18019
tuned;
webertj [Fri, 28 Oct 2005 20:18:37 +0200] rev 18018
unnecessary imports removed
urbanc [Fri, 28 Oct 2005 18:53:26 +0200] rev 18017
fixed case names in the weak induction principle and
changed name from "induct" to "induct_weak"
berghofe [Fri, 28 Oct 2005 18:22:26 +0200] rev 18016
Implemented proof of weak induction theorem.
berghofe [Fri, 28 Oct 2005 17:59:07 +0200] rev 18015
Added "deepen" method.
haftmann [Fri, 28 Oct 2005 17:27:49 +0200] rev 18014
circumvented smlnj value restriction
haftmann [Fri, 28 Oct 2005 17:27:04 +0200] rev 18013
added extraction interface for code generator
urbanc [Fri, 28 Oct 2005 16:43:46 +0200] rev 18012
Added (optional) arguments to the tactics
perm_eq_simp and supports_simp. They now
follow the "simp"-way and use the syntax:
apply(supports_simp simp add: thms)
etc.
haftmann [Fri, 28 Oct 2005 16:35:40 +0200] rev 18011
cleaned up nth, nth_update, nth_map and nth_string functions
berghofe [Fri, 28 Oct 2005 13:52:57 +0200] rev 18010
Removed legacy prove_goalw_cterm command.
paulson [Fri, 28 Oct 2005 12:22:34 +0200] rev 18009
got rid of obsolete prove_goalw_cterm
haftmann [Fri, 28 Oct 2005 09:36:19 +0200] rev 18008
swapped add_datatype result
haftmann [Fri, 28 Oct 2005 09:35:04 +0200] rev 18007
removed obfuscating PStrStrTab
haftmann [Fri, 28 Oct 2005 08:40:55 +0200] rev 18006
reachable - abandoned foldl_map in favor of fold_map
mengj [Fri, 28 Oct 2005 02:30:53 +0200] rev 18005
Added Tools/res_hol_clause.ML
mengj [Fri, 28 Oct 2005 02:30:12 +0200] rev 18004
Added a new file res_hol_clause.ML to Reconstruction.thy. This file is used to translate HOL formulae into FOL clauses.
mengj [Fri, 28 Oct 2005 02:29:01 +0200] rev 18003
Added "writeln_strs" to the signature
mengj [Fri, 28 Oct 2005 02:28:20 +0200] rev 18002
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.
mengj [Fri, 28 Oct 2005 02:27:19 +0200] rev 18001
Added new functions to handle HOL goals and lemmas.
Added a funtion to send types and sorts information to ATP: they are clauses written to a separate file.
Removed several functions definitions, and combined them with those in other files.