# HG changeset patch
# User bulwahn
# Date 1294420242 -3600
# Node ID cb2e3e651893eb98875be4bb86638e4bb3378f7c
# Parent  edbf0a86fb1cb2c5f5711aa1ca9379f1f32fed36
adopting proofs due to new list comprehension to set comprehension simproc

diff -r edbf0a86fb1c -r cb2e3e651893 src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Fri Jan 07 18:10:35 2011 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy	Fri Jan 07 18:10:42 2011 +0100
@@ -3585,9 +3585,9 @@
     thus "(UNION M (\<lambda> (a,b,c). set (f (a,b,c)))) = (UNION M (\<lambda> (a,b,c). set (g a b c)))"
       by (auto simp add: split_def)
   qed
-  have "?SS (Floor a) = UNION (?SS a) (\<lambda>x. set (?ff x))" 
-    by (auto simp add: foldl_conv_concat)
-  also have "\<dots> = UNION (?SS a) (\<lambda> (p,n,s). set (?ff (p,n,s)))" by auto
+  have "?SS (Floor a) = UNION (?SS a) (\<lambda>x. set (?ff x))"
+    by (auto simp add: foldl_conv_concat simp del: iupt.simps)
+  also have "\<dots> = UNION (?SS a) (\<lambda> (p,n,s). set (?ff (p,n,s)))" by blast
   also have "\<dots> = 
     ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un 
     (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un 
@@ -3743,8 +3743,8 @@
       by (auto simp add: split_def)
   qed
 
-  have "?SS (Floor a) = UNION (?SS a) (\<lambda>x. set (?ff x))" by (auto simp add: foldl_conv_concat) 
-  also have "\<dots> = UNION (?SS a) (\<lambda> (p,n,s). set (?ff (p,n,s)))" by auto
+  have "?SS (Floor a) = UNION (?SS a) (\<lambda>x. set (?ff x))" by (auto simp add: foldl_conv_concat simp del: iupt.simps) 
+  also have "\<dots> = UNION (?SS a) (\<lambda> (p,n,s). set (?ff (p,n,s)))" by blast
   also have "\<dots> = 
     ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un 
     (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un 
diff -r edbf0a86fb1c -r cb2e3e651893 src/HOL/MicroJava/BV/Typing_Framework_JVM.thy
--- a/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Fri Jan 07 18:10:35 2011 +0100
+++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Fri Jan 07 18:10:42 2011 +0100
@@ -89,14 +89,14 @@
   apply clarsimp
   apply (erule disjE)
    apply (fastsimp dest: field_fields fields_is_type)
-  apply (simp add: match_some_entry split: split_if_asm)
+  apply (simp add: match_some_entry image_iff)
   apply (rule_tac x=1 in exI)
   apply fastsimp
 
   apply clarsimp
   apply (erule disjE)
    apply fastsimp
-  apply (simp add: match_some_entry split: split_if_asm)
+  apply (simp add: match_some_entry image_iff)
   apply (rule_tac x=1 in exI)
   apply fastsimp