--- 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));