src/HOL/NanoJava/State.thy
changeset 35431 8758fe1fc9f8
parent 35417 47ee18b6ae32
child 42463 f270e3e18be5
     1.1 --- a/src/HOL/NanoJava/State.thy	Wed Mar 03 00:32:14 2010 +0100
     1.2 +++ b/src/HOL/NanoJava/State.thy	Wed Mar 03 00:33:02 2010 +0100
     1.3 @@ -23,9 +23,8 @@
     1.4          obj = "cname \<times> fields"
     1.5  
     1.6  translations
     1.7 -
     1.8 -  "fields" \<leftharpoondown> (type)"fname => val option"
     1.9 -  "obj"    \<leftharpoondown> (type)"cname \<times> fields"
    1.10 +  (type) "fields" \<leftharpoondown> (type) "fname => val option"
    1.11 +  (type) "obj"    \<leftharpoondown> (type) "cname \<times> fields"
    1.12  
    1.13  definition init_vars :: "('a \<rightharpoonup> 'b) => ('a \<rightharpoonup> val)" where
    1.14   "init_vars m == Option.map (\<lambda>T. Null) o m"
    1.15 @@ -40,10 +39,9 @@
    1.16            locals :: locals
    1.17  
    1.18  translations
    1.19 -
    1.20 -  "heap"   \<leftharpoondown> (type)"loc   => obj option"
    1.21 -  "locals" \<leftharpoondown> (type)"vname => val option"
    1.22 -  "state" \<leftharpoondown> (type)"(|heap :: heap, locals :: locals|)"
    1.23 +  (type) "heap" \<leftharpoondown> (type) "loc => obj option"
    1.24 +  (type) "locals" \<leftharpoondown> (type) "vname => val option"
    1.25 +  (type) "state" \<leftharpoondown> (type) "(|heap :: heap, locals :: locals|)"
    1.26  
    1.27  definition del_locs :: "state => state" where
    1.28   "del_locs s \<equiv> s (| locals := empty |)"