--- a/src/FOL/blastdata.ML Mon Nov 14 16:26:40 2005 +0100
+++ b/src/FOL/blastdata.ML Mon Nov 14 18:25:34 2005 +0100
@@ -3,7 +3,6 @@
structure Blast_Data =
struct
type claset = Cla.claset
- val is_hol = false
val notE = notE
val ccontr = ccontr
val contr_tac = Cla.contr_tac
--- a/src/HOL/blastdata.ML Mon Nov 14 16:26:40 2005 +0100
+++ b/src/HOL/blastdata.ML Mon Nov 14 18:25:34 2005 +0100
@@ -16,7 +16,6 @@
structure Blast_Data =
struct
type claset = Classical.claset
- val is_hol = true
val notE = notE
val ccontr = ccontr
val contr_tac = Classical.contr_tac
--- a/src/Provers/blast.ML Mon Nov 14 16:26:40 2005 +0100
+++ b/src/Provers/blast.ML Mon Nov 14 18:25:34 2005 +0100
@@ -8,6 +8,9 @@
SKOLEMIZES ReplaceI WRONGLY: allow new vars in prems, or forbid such rules??
Needs explicit instantiation of assumptions?
+Given the typeargs system, constructor Const could be eliminated, with
+TConst replaced by a constructor that takes the typargs list as an argument.
+However, Const is heavily used for logical connectives.
Blast_tac is often more powerful than fast_tac, but has some limitations.
Blast_tac...
@@ -48,7 +51,6 @@
sig
type claset
val notE : thm (* [| ~P; P |] ==> R *)
- val is_hol : bool (*Is this HOL or FOL/ZF?*)
val ccontr : thm
val contr_tac : int -> tactic
val dup_intr : thm -> thm
@@ -156,7 +158,11 @@
fun isGoal (Const"*Goal*" $ _) = true
| isGoal _ = false;
-val boolT = if Data.is_hol then "bool" else "o";
+val boolT =
+ case term_vars (hd (prems_of Data.notE)) of
+ [Term.Var(_, Type(s, []))] => s
+ | _ => error ("Theorem notE is ill-formed: " ^ string_of_thm Data.notE);
+
val Trueprop = Term.Const("Trueprop", Type(boolT,[])-->propT);
fun mk_tprop P = Term.$ (Trueprop, P);