--- a/src/HOL/HOL.ML Fri Oct 13 09:02:21 2006 +0200
+++ b/src/HOL/HOL.ML Fri Oct 13 12:32:44 2006 +0200
@@ -1,5 +1,6 @@
(* legacy ML bindings *)
+val prop_cs = HOL.claset_prop;
val HOL_cs = HOL.claset;
val HOL_basic_ss = HOL.simpset_basic;
val HOL_ss = HOL.simpset;
@@ -18,6 +19,8 @@
val claset = Classical.claset;
val simpset = Simplifier.simpset;
val simplify = Simplifier.simplify;
+open Hypsubst;
+open BasicClassical;
open Clasimp;
val ext = thm "ext"
--- a/src/HOL/HOL.thy Fri Oct 13 09:02:21 2006 +0200
+++ b/src/HOL/HOL.thy Fri Oct 13 12:32:44 2006 +0200
@@ -863,10 +863,63 @@
use "cladata.ML"
setup Hypsubst.hypsubst_setup
-setup {* ContextRules.addSWrapper (fn tac => HOL.hyp_subst_tac' ORELSE' tac) *}
+setup {*
+let
+ (*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 Hypsubst.hyp_subst_tac i thm else no_tac thm;
+in
+ ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)
+end
+*}
setup Classical.setup
setup ResAtpset.setup
-setup {* fn thy => (Classical.change_claset_of thy (K HOL.claset); thy) *}
+
+declare iffI [intro!]
+ and notI [intro!]
+ and impI [intro!]
+ and disjCI [intro!]
+ and conjI [intro!]
+ and TrueI [intro!]
+ and refl [intro!]
+
+declare iffCE [elim!]
+ and FalseE [elim!]
+ and impCE [elim!]
+ and disjE [elim!]
+ and conjE [elim!]
+ and conjE [elim!]
+
+ML {*
+structure HOL =
+struct
+
+open HOL;
+
+val claset_prop = Classical.claset_of (the_context ());
+
+end;
+*}
+
+declare ex_ex1I [intro!]
+ and allI [intro!]
+ and the_equality [intro]
+ and exI [intro]
+
+declare exE [elim!]
+ allE [elim]
+
+ML {*
+structure HOL =
+struct
+
+open HOL;
+
+val claset = Classical.claset_of (the_context ());
+
+end;
+*}
lemma contrapos_np: "~ Q ==> (~ P ==> Q) ==> P"
apply (erule swap)
@@ -901,6 +954,9 @@
fun case_tac a = res_inst_tac [("P", a)] case_split;
+val Blast_tac = Blast.Blast_tac;
+val blast_tac = Blast.blast_tac;
+
end;
*}
--- a/src/HOL/blastdata.ML Fri Oct 13 09:02:21 2006 +0200
+++ b/src/HOL/blastdata.ML Fri Oct 13 12:32:44 2006 +0200
@@ -15,13 +15,3 @@
end;
structure Blast = BlastFun(Blast_Data);
-
-structure HOL =
-struct
-
-open HOL;
-
-val Blast_tac = Blast.Blast_tac;
-val blast_tac = Blast.blast_tac;
-
-end;
\ No newline at end of file
--- 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;