src/HOL/IMP/Fold.thy
changeset 51506 cd573f1a82b2
parent 48909 b2dea007e55e
child 51514 9bed72e55475
--- a/src/HOL/IMP/Fold.thy	Sun Mar 24 16:19:54 2013 +0100
+++ b/src/HOL/IMP/Fold.thy	Mon Mar 25 13:50:50 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"