tidied
authorpaulson
Fri Dec 03 15:27:47 2004 +0100 (2004-12-03)
changeset 15369090b16d6c6e0
parent 15368 79f624f97f7f
child 15370 05b03ea0f18d
tidied
src/HOL/Map.thy
     1.1 --- a/src/HOL/Map.thy	Fri Dec 03 12:52:24 2004 +0100
     1.2 +++ b/src/HOL/Map.thy	Fri Dec 03 15:27:47 2004 +0100
     1.3 @@ -219,16 +219,18 @@
     1.4  apply auto
     1.5  done
     1.6  
     1.7 -lemma map_of_SomeD [rule_format (no_asm)]: "map_of xs k = Some y --> (k,y):set xs"
     1.8 +lemma map_of_SomeD [rule_format]: "map_of xs k = Some y --> (k,y):set xs"
     1.9  by (induct "xs", auto)
    1.10  
    1.11 -lemma map_of_mapk_SomeI [rule_format (no_asm)]: "inj f ==> map_of t k = Some x -->  
    1.12 -   map_of (map (split (%k. Pair (f k))) t) (f k) = Some x"
    1.13 +lemma map_of_mapk_SomeI [rule_format]:
    1.14 +     "inj f ==> map_of t k = Some x -->  
    1.15 +        map_of (map (split (%k. Pair (f k))) t) (f k) = Some x"
    1.16  apply (induct "t")
    1.17  apply  (auto simp add: inj_eq)
    1.18  done
    1.19  
    1.20 -lemma weak_map_of_SomeI [rule_format (no_asm)]: "(k, x) : set l --> (? x. map_of l k = Some x)"
    1.21 +lemma weak_map_of_SomeI [rule_format]:
    1.22 +     "(k, x) : set l --> (\<exists>x. map_of l k = Some x)"
    1.23  by (induct "l", auto)
    1.24  
    1.25  lemma map_of_filter_in: 
    1.26 @@ -454,7 +456,7 @@
    1.27  by (unfold dom_def, auto)
    1.28  (* declare domI [intro]? *)
    1.29  
    1.30 -lemma domD: "a : dom m ==> ? b. m a = Some b"
    1.31 +lemma domD: "a : dom m ==> \<exists>b. m a = Some b"
    1.32  by (unfold dom_def, auto)
    1.33  
    1.34  lemma domIff[iff]: "(a : dom m) = (m a ~= None)"