diff -r 20ca66539bef -r 0f89104dd377 src/ZF/Coind/Map.thy
--- a/src/ZF/Coind/Map.thy	Wed Jul 10 16:07:52 2002 +0200
+++ b/src/ZF/Coind/Map.thy	Wed Jul 10 16:54:07 2002 +0200
@@ -105,10 +105,8 @@
 
 lemma pmap_owrI: 
   "[| m \<in> PMap(A,B); a \<in> A; b \<in> B |]  ==> map_owr(m,a,b):PMap(A,B)"
-apply (unfold map_owr_def PMap_def TMap_def)
-apply safe
-apply (simp_all add: if_iff)
-apply auto
+apply (unfold map_owr_def PMap_def TMap_def, safe)
+apply (simp_all add: if_iff, auto)
 (*Remaining subgoal*)
 apply (rule excluded_middle [THEN disjE])
 apply (erule image_Sigma1)
@@ -130,8 +128,7 @@
   "[| m \<in> PMap(A,B); a \<in> domain(m) |] ==> map_app(m,a):B"
 apply (unfold PMap_def)
 apply (frule tmap_app_notempty, assumption)
-apply (drule tmap_appI)
-apply auto
+apply (drule tmap_appI, auto)
 done
 
 (** domain **)