# HG changeset patch
# User wenzelm
# Date 965123907 -7200
# Node ID f11bece4e2db06d16cc248f644cf5a497cea36af
# Parent  7e377f912629cfa30ea1e82e10ec5c1dc5903770
added all_eq, imp_eq (for blast);

diff -r 7e377f912629 -r f11bece4e2db src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Aug 01 11:58:14 2000 +0200
+++ b/src/HOL/HOL.thy	Tue Aug 01 11:58:27 2000 +0200
@@ -193,6 +193,26 @@
 
 use "HOL_lemmas.ML"	setup attrib_setup
 use "cladata.ML"	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
+
 use "blastdata.ML"	setup Blast.setup
 use "simpdata.ML"	setup Simplifier.setup
 			setup "Simplifier.method_setup Splitter.split_modifiers"