
diff -r 37dfd7af2746 -r 9dba9c7872c9 src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Tue Sep 19 15:22:29 2006 +0200
+++ b/src/HOL/Inductive.thy	Tue Sep 19 15:22:35 2006 +0200
@@ -70,6 +70,26 @@
   Ball_def Bex_def
   induct_rulify_fallback
 
+lemma False_meta_all:
+  "Trueprop False \<equiv> (\<And>P\<Colon>bool. P)"
+proof
+  fix P
+  assume False
+  then show P ..
+next
+  assume "\<And>P\<Colon>bool. P"
+  then show "False" ..
+qed
+
+lemma not_eq_False:
+  assumes not_eq: "x \<noteq> y"
+  and eq: "x == y"
+  shows False
+  using not_eq eq by auto
+
+lemmas not_eq_quodlibet =
+  not_eq_False [simplified False_meta_all]
+
 
 subsection {* Inductive datatypes and primitive recursion *}
 




