# HG changeset patch
# User blanchet
# Date 1272628809 -7200
# Node ID 16ec4fe058cb70c8c835a3ef6e60b627353748a5
# Parent  9bebcb40599f3884ad79a97f8e4fefb5549f1345
minor improvements

diff -r 9bebcb40599f -r 16ec4fe058cb src/HOL/Metis_Examples/Abstraction.thy
--- a/src/HOL/Metis_Examples/Abstraction.thy	Fri Apr 30 13:58:35 2010 +0200
+++ b/src/HOL/Metis_Examples/Abstraction.thy	Fri Apr 30 14:00:09 2010 +0200
@@ -66,13 +66,11 @@
 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>x w. (\<lambda>R. w (x R)) = x -` w" by (metis vimage_Collect_eq Collect_def)
-  have F3: "\<forall>v w y. v \<in> w -` op = y \<longrightarrow> w v = y" by (metis F1 vimage_singleton_eq)
-  have F4: "b \<in> {R. a = f R}" by (metis A1 mem_Sigma_iff)
-  have F5: "a \<in> A" by (metis A1 mem_Sigma_iff)
-  have "b \<in> f -` op = a" by (metis F2 F4 Collect_def)
-  hence "f b = a" by (metis F3)
-  thus "a \<in> A \<and> a = f b" by (metis F5)
+  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 *)
diff -r 9bebcb40599f -r 16ec4fe058cb src/HOL/Metis_Examples/BT.thy
--- a/src/HOL/Metis_Examples/BT.thy	Fri Apr 30 13:58:35 2010 +0200
+++ b/src/HOL/Metis_Examples/BT.thy	Fri Apr 30 14:00:09 2010 +0200
@@ -133,7 +133,7 @@
 apply (rule ext) 
 apply (induct_tac y)
  apply (metis bt_map.simps(1))
-by (metis COMBI_def bt_map.simps(2))
+by (metis bt_map.simps(2))
 
 declare [[ atp_problem_prefix = "BT__bt_map_appnd" ]]