src/HOL/HOL.thy

 
 (* theory and package setup *)
 
 use "HOL_lemmas.ML"
 
+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" by (rule allI)
+next
+  assume "ALL 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 impI) (rule r)
+next
+  assume "A --> B" and A
+  thus B by (rule mp)
+qed
+
+lemmas atomize = all_eq imp_eq
+
 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" ..
-next
-  assume "ALL x. P x"
-  thus "!!x. P x" ..
-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)
-next
-  assume "A --> B" and A
-  thus B ..
-qed
-
-lemmas atomize = all_eq imp_eq
-
 use "blastdata.ML"
 setup Blast.setup
 
 use "simpdata.ML"
 setup Simplifier.setup