# HG changeset patch
# User kleing
# Date 1364215850 -3600
# Node ID cd573f1a82b2c78d99a7da4be98c6a9afd0f346b
# Parent  9e91959a8cfcf4961d8ee4ea1be40b45c4a33320
removed obsolete uses of ext

diff -r 9e91959a8cfc -r cd573f1a82b2 src/HOL/IMP/Fold.thy
--- 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"