--- a/src/FOL/FOL.thy Fri Nov 03 21:29:56 2000 +0100
+++ b/src/FOL/FOL.thy Fri Nov 03 21:31:11 2000 +0100
@@ -24,31 +24,31 @@
subsection {* Setup of several proof tools *}
use "FOL_lemmas1.ML"
-use "cladata.ML"
-setup Cla.setup
-setup clasetup
lemma all_eq: "(!!x. P(x)) == Trueprop (ALL x. P(x))"
proof (rule equal_intr_rule)
assume "!!x. P(x)"
- show "ALL x. P(x)" ..
+ show "ALL x. P(x)" by (rule allI)
next
assume "ALL x. P(x)"
- thus "!!x. P(x)" ..
+ thus "!!x. P(x)" by (rule allE)
qed
lemma imp_eq: "(A ==> B) == Trueprop (A --> B)"
proof (rule equal_intr_rule)
assume r: "A ==> B"
- show "A --> B"
- by (rule) (rule r)
+ show "A --> B" by (rule impI) (rule r)
next
assume "A --> B" and A
- thus B ..
+ thus B by (rule mp)
qed
lemmas atomize = all_eq imp_eq
+use "cladata.ML"
+setup Cla.setup
+setup clasetup
+
use "blastdata.ML"
setup Blast.setup
use "FOL_lemmas2.ML"
--- a/src/FOL/cladata.ML Fri Nov 03 21:29:56 2000 +0100
+++ b/src/FOL/cladata.ML Fri Nov 03 21:31:11 2000 +0100
@@ -24,12 +24,11 @@
val classical = classical
val sizef = size_of_thm
val hyp_subst_tacs=[hyp_subst_tac]
+ val atomize = thms "atomize"
end;
structure Cla = ClassicalFun(Classical_Data);
structure BasicClassical: BASIC_CLASSICAL = Cla; open BasicClassical;
-structure Obtain = ObtainFun(val atomic_thesis = FOLogic.atomic_Trueprop and
- that_atts = [Simplifier.simp_add_local, Cla.haz_intro_local]);
(*Better for fast_tac: needs no quantifier duplication!*)
--- a/src/HOL/HOL.thy Fri Nov 03 21:29:56 2000 +0100
+++ b/src/HOL/HOL.thy Fri Nov 03 21:31:11 2000 +0100
@@ -196,32 +196,31 @@
use "HOL_lemmas.ML"
-use "cladata.ML"
-setup hypsubst_setup
-setup Classical.setup
-setup clasetup
-
lemma all_eq: "(!!x. P x) == Trueprop (ALL x. P x)"
proof (rule equal_intr_rule)
assume "!!x. P x"
- show "ALL x. P x" ..
+ show "ALL x. P x" by (rule allI)
next
assume "ALL x. P x"
- thus "!!x. P x" ..
+ thus "!!x. P x" by (rule allE)
qed
lemma imp_eq: "(A ==> B) == Trueprop (A --> B)"
proof (rule equal_intr_rule)
assume r: "A ==> B"
- show "A --> B"
- by (rule) (rule r)
+ show "A --> B" by (rule impI) (rule r)
next
assume "A --> B" and A
- thus B ..
+ thus B by (rule mp)
qed
lemmas atomize = all_eq imp_eq
+use "cladata.ML"
+setup hypsubst_setup
+setup Classical.setup
+setup clasetup
+
use "blastdata.ML"
setup Blast.setup
--- a/src/HOL/cladata.ML Fri Nov 03 21:29:56 2000 +0100
+++ b/src/HOL/cladata.ML Fri Nov 03 21:31:11 2000 +0100
@@ -47,6 +47,7 @@
val classical = classical
val sizef = size_of_thm
val hyp_subst_tacs=[hyp_subst_tac]
+ val atomize = thms "atomize"
end;
structure Classical = ClassicalFun(Classical_Data);
@@ -56,9 +57,6 @@
bind_thm ("contrapos_np", inst "Pa" "?Q" swap);
-structure Obtain = ObtainFun(val atomic_thesis = HOLogic.atomic_Trueprop and
- that_atts = [Simplifier.simp_add_local, Classical.haz_intro_local]);
-
(*Propositional rules*)
val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI]
addSEs [conjE,disjE,impCE,FalseE,iffCE];