--- 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 **)