src/HOL/cladata.ML

--- a/src/HOL/cladata.ML	Fri Oct 13 09:02:21 2006 +0200
+++ b/src/HOL/cladata.ML	Fri Oct 13 12:32:44 2006 +0200
@@ -34,25 +34,3 @@
 
 structure Classical = ClassicalFun(Classical_Data);
 structure BasicClassical: BASIC_CLASSICAL = Classical; 
-
-structure HOL =
-struct
-
-open HOL;
-open Hypsubst;
-open BasicClassical;
-
-(*prevent substitution on bool*)
-fun hyp_subst_tac' i thm = if i <= Thm.nprems_of thm andalso
-  Term.exists_Const (fn ("op =", Type (_, [T, _])) => T <> Type ("bool", []) | _ => false)
-    (nth (Thm.prems_of thm) (i - 1)) then hyp_subst_tac i thm else no_tac thm;
-
-(*Propositional rules*)
-val prop_cs = empty_cs addSIs [HOL.refl, HOL.TrueI, HOL.conjI, HOL.disjCI, HOL.impI, HOL.notI, HOL.iffI]
-                       addSEs [HOL.conjE, HOL.disjE, HOL.impCE, HOL.FalseE, HOL.iffCE];
-
-(*Quantifier rules*)
-val claset = prop_cs addSIs [HOL.allI, HOL.ex_ex1I] addIs [HOL.exI, HOL.the_equality] 
-                     addSEs [HOL.exE] addEs [HOL.allE];
-
-end;