# HG changeset patch
# User haftmann
# Date 1158672155 -7200
# Node ID 9dba9c7872c9ceec453c7db3f995f4b2526fec86
# Parent  37dfd7af2746196a331741bd27f95ad6f365862f
added auxiliary lemma for code generation 2

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