author berghofe Wed, 07 May 2008 10:59:34 +0200 changeset 26819 56036226028b parent 26818 b4a24433154e child 26820 2909150bd614
Replaced union_empty2 by Un_empty_right.
```--- a/src/HOL/MetisExamples/Abstraction.thy	Wed May 07 10:59:33 2008 +0200
+++ b/src/HOL/MetisExamples/Abstraction.thy	Wed May 07 10:59:34 2008 +0200
@@ -69,7 +69,7 @@

(*single-step*)
lemma "(a,b) \<in> (SIGMA x: A. {y. x = f y}) ==> a \<in> A & a = f b"

lemma "(a,b) \<in> (SIGMA x: A. {y. x = f y}) ==> a \<in> A & a = f b"
@@ -88,7 +88,7 @@
have 5: "(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type) (b\<Colon>'b\<Colon>type) \<noteq> (a\<Colon>'a\<Colon>type)"
by (metis 1 2)
have 6: "(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type) (b\<Colon>'b\<Colon>type) = (a\<Colon>'a\<Colon>type)"
-  by (metis 4 vimage_singleton_eq insert_def singleton_conv2 union_empty2 vimage_Collect_eq vimage_def)
+  by (metis 4 vimage_singleton_eq insert_def singleton_conv2 Un_empty_right vimage_Collect_eq vimage_def)
show "False"
by (metis 5 6)
qed
@@ -100,7 +100,7 @@
have 1: "b \<in> Collect (COMBB (op = a) f)"