# HG changeset patch
# User haftmann
# Date 1160735564 -7200
# Node ID 0eae3fb489361be11647539e5475b50087319873
# Parent  330a8a6dd53ce554f52e4acb53aaa6f125c11348
lifted claset setup from ML to Isar level

diff -r 330a8a6dd53c -r 0eae3fb48936 src/HOL/HOL.ML
--- 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"
diff -r 330a8a6dd53c -r 0eae3fb48936 src/HOL/HOL.thy
--- 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;
 *}
 
diff -r 330a8a6dd53c -r 0eae3fb48936 src/HOL/blastdata.ML
--- 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
diff -r 330a8a6dd53c -r 0eae3fb48936 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;