# HG changeset patch
# User paulson
# Date 1102084067 -3600
# Node ID 090b16d6c6e04a9189ccf7fdeffb450e7897625d
# Parent  79f624f97f7fde972610ab261a350e5c0020f4dd
tidied

diff -r 79f624f97f7f -r 090b16d6c6e0 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Fri Dec 03 12:52:24 2004 +0100
+++ b/src/HOL/Map.thy	Fri Dec 03 15:27:47 2004 +0100
@@ -219,16 +219,18 @@
 apply auto
 done
 
-lemma map_of_SomeD [rule_format (no_asm)]: "map_of xs k = Some y --> (k,y):set xs"
+lemma map_of_SomeD [rule_format]: "map_of xs k = Some y --> (k,y):set xs"
 by (induct "xs", auto)
 
-lemma map_of_mapk_SomeI [rule_format (no_asm)]: "inj f ==> map_of t k = Some x -->  
-   map_of (map (split (%k. Pair (f k))) t) (f k) = Some x"
+lemma map_of_mapk_SomeI [rule_format]:
+     "inj f ==> map_of t k = Some x -->  
+        map_of (map (split (%k. Pair (f k))) t) (f k) = Some x"
 apply (induct "t")
 apply  (auto simp add: inj_eq)
 done
 
-lemma weak_map_of_SomeI [rule_format (no_asm)]: "(k, x) : set l --> (? x. map_of l k = Some x)"
+lemma weak_map_of_SomeI [rule_format]:
+     "(k, x) : set l --> (\<exists>x. map_of l k = Some x)"
 by (induct "l", auto)
 
 lemma map_of_filter_in: 
@@ -454,7 +456,7 @@
 by (unfold dom_def, auto)
 (* declare domI [intro]? *)
 
-lemma domD: "a : dom m ==> ? b. m a = Some b"
+lemma domD: "a : dom m ==> \<exists>b. m a = Some b"
 by (unfold dom_def, auto)
 
 lemma domIff[iff]: "(a : dom m) = (m a ~= None)"