# HG changeset patch
# User wenzelm
# Date 1364216879 -3600
# Node ID 193ba70666bd65dd0db6ada0d21653ba073d4bdb
# Parent  cd573f1a82b2c78d99a7da4be98c6a9afd0f346b# Parent  e768a64ee53a3a0be4f5e3d445188caa3e627836
merged

diff -r e768a64ee53a -r 193ba70666bd src/HOL/IMP/Fold.thy
--- 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"