merged

--- a/src/HOL/IMP/Fold.thy	Mon Mar 25 14:04:01 2013 +0100
+++ b/src/HOL/IMP/Fold.thy	Mon Mar 25 14:07:59 2013 +0100
@@ -75,7 +75,7 @@
    and "\<forall>x. (t2 |` S) x = (t |` S) x" by auto
   thus ?thesis
     by (auto simp: merge_def restrict_map_def
-             split: if_splits intro: ext)
+             split: if_splits)
 qed
 
 
@@ -205,7 +205,7 @@
 
 lemma approx_empty [simp]:
   "approx empty = (\<lambda>_. True)"
-  by (auto intro!: ext simp: approx_def)
+  by (auto simp: approx_def)
 
 lemma equiv_sym:
   "c \<sim> c' \<longleftrightarrow> c' \<sim> c"