src/HOL/NanoJava/State.thy
changeset 42463 f270e3e18be5
parent 35431 8758fe1fc9f8
child 55466 786edc984c98
     1.1 --- a/src/HOL/NanoJava/State.thy	Fri Apr 22 15:57:43 2011 +0200
     1.2 +++ b/src/HOL/NanoJava/State.thy	Sat Apr 23 13:00:19 2011 +0200
     1.3 @@ -17,9 +17,10 @@
     1.4    = Null        --{* null reference *}
     1.5    | Addr loc    --{* address, i.e. location of object *}
     1.6  
     1.7 -types   fields
     1.8 +type_synonym fields
     1.9          = "(fname \<rightharpoonup> val)"
    1.10  
    1.11 +type_synonym
    1.12          obj = "cname \<times> fields"
    1.13  
    1.14  translations
    1.15 @@ -30,8 +31,8 @@
    1.16   "init_vars m == Option.map (\<lambda>T. Null) o m"
    1.17    
    1.18  text {* private: *}
    1.19 -types   heap   = "loc   \<rightharpoonup> obj"
    1.20 -        locals = "vname \<rightharpoonup> val"  
    1.21 +type_synonym heap = "loc   \<rightharpoonup> obj"
    1.22 +type_synonym locals = "vname \<rightharpoonup> val"  
    1.23  
    1.24  text {* private: *}
    1.25  record  state