--- 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"