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