# HG changeset patch
# User blanchet
# Date 1305206959 -7200
# Node ID ebf603e5406114d669f5d01eb6cfa04faa9caf14
# Parent  6b7ef9b724fdf40edf77e4ac42e9f9a74e3fbe74
remove problematic Isar proof

diff -r 6b7ef9b724fd -r ebf603e54061 src/HOL/Metis_Examples/Abstraction.thy
--- a/src/HOL/Metis_Examples/Abstraction.thy	Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Metis_Examples/Abstraction.thy	Thu May 12 15:29:19 2011 +0200
@@ -68,18 +68,6 @@
 lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b"
 proof -
   assume A1: "(a, b) \<in> (SIGMA x:A. {y. x = f y})"
-  have F1: "\<forall>u. {u} = op = u" by (metis singleton_conv2 Collect_def)
-  have F2: "\<forall>y w v. v \<in> w -` op = y \<longrightarrow> w v = y"
-    by (metis F1 vimage_singleton_eq)
-  have F3: "\<forall>x w. (\<lambda>R. w (x R)) = x -` w"
-    by (metis vimage_Collect_eq Collect_def)
-  show "a \<in> A \<and> a = f b" by (metis A1 F2 F3 mem_Sigma_iff Collect_def)
-qed
-
-(* Alternative structured proof *)
-lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b"
-proof -
-  assume A1: "(a, b) \<in> (SIGMA x:A. {y. x = f y})"
   hence F1: "a \<in> A" by (metis mem_Sigma_iff)
   have "b \<in> {R. a = f R}" by (metis A1 mem_Sigma_iff)
   hence F2: "b \<in> (\<lambda>R. a = f R)" by (metis Collect_def)