# HG changeset patch
# User wenzelm
# Date 973283471 -3600
# Node ID a092ae7bb2a6865f084f6bf4a07b42fea088b484
# Parent  1fb807260ff1bf142a0b1c3f9e4a9aedfa99002e
"atomize" for classical tactics;

diff -r 1fb807260ff1 -r a092ae7bb2a6 src/FOL/FOL.thy
--- 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"
diff -r 1fb807260ff1 -r a092ae7bb2a6 src/FOL/cladata.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!*)
diff -r 1fb807260ff1 -r a092ae7bb2a6 src/HOL/HOL.thy
--- 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
 
diff -r 1fb807260ff1 -r a092ae7bb2a6 src/HOL/cladata.ML
--- 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];