src/FOL/cladata.ML
changeset 21539 c5cf9243ad62
parent 18708 4b3dadb4fe33
child 22127 025dfa637f78
--- a/src/FOL/cladata.ML	Sun Nov 26 23:09:25 2006 +0100
+++ b/src/FOL/cladata.ML	Sun Nov 26 23:43:53 2006 +0100
@@ -13,7 +13,7 @@
   struct
   val mp        = mp
   val not_elim  = notE
-  val classical = classical
+  val classical = thm "classical"
   val sizef     = size_of_thm
   val hyp_subst_tacs=[hyp_subst_tac]
   end;
@@ -22,25 +22,15 @@
 structure BasicClassical: BASIC_CLASSICAL = Cla; open BasicClassical;
 
 
-(*Better for fast_tac: needs no quantifier duplication!*)
-qed_goal "alt_ex1E" IFOL.thy
-    "[| EX! x. P(x);                                              \
-\       !!x. [| P(x);  ALL y y'. P(y) & P(y') --> y=y' |] ==> R  \
-\    |] ==> R"
- (fn major::prems =>
-  [ (rtac (major RS ex1E) 1),
-    (REPEAT (ares_tac (allI::prems) 1)),
-    (etac (dup_elim allE) 1),
-    (IntPr.fast_tac 1)]);
-
 
 (*Propositional rules*)
-val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI] 
-                       addSEs [conjE,disjE,impCE,FalseE,iffCE];
+val prop_cs = empty_cs
+  addSIs [refl, TrueI, conjI, thm "disjCI", impI, notI, iffI]
+  addSEs [conjE, disjE, thm "impCE", FalseE, thm "iffCE"];
 
 (*Quantifier rules*)
-val FOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI] 
-                     addSEs [exE,alt_ex1E] addEs [allE];
+val FOL_cs = prop_cs addSIs [allI, thm "ex_ex1I"] addIs [exI]
+                     addSEs [exE, thm "alt_ex1E"] addEs [allE];
 
 val cla_setup = (fn thy => (change_claset_of thy (fn _ => FOL_cs); thy));