src/HOL/Bali/State.thy
changeset 35431 8758fe1fc9f8
parent 35416 d8d7d1b785af
child 37956 ee939247b2fb
     1.1 --- a/src/HOL/Bali/State.thy	Wed Mar 03 00:32:14 2010 +0100
     1.2 +++ b/src/HOL/Bali/State.thy	Wed Mar 03 00:33:02 2010 +0100
     1.3 @@ -33,10 +33,10 @@
     1.4            "values" :: "(vn, val) table"      
     1.5  
     1.6  translations 
     1.7 -  "fspec" <= (type) "vname \<times> qtname" 
     1.8 -  "vn"    <= (type) "fspec + int"
     1.9 -  "obj"   <= (type) "\<lparr>tag::obj_tag, values::vn \<Rightarrow> val option\<rparr>"
    1.10 -  "obj"   <= (type) "\<lparr>tag::obj_tag, values::vn \<Rightarrow> val option,\<dots>::'a\<rparr>"
    1.11 +  (type) "fspec" <= (type) "vname \<times> qtname" 
    1.12 +  (type) "vn"    <= (type) "fspec + int"
    1.13 +  (type) "obj"   <= (type) "\<lparr>tag::obj_tag, values::vn \<Rightarrow> val option\<rparr>"
    1.14 +  (type) "obj"   <= (type) "\<lparr>tag::obj_tag, values::vn \<Rightarrow> val option,\<dots>::'a\<rparr>"
    1.15  
    1.16  definition the_Arr :: "obj option \<Rightarrow> ty \<times> int \<times> (vn, val) table" where
    1.17   "the_Arr obj \<equiv> SOME (T,k,t). obj = Some \<lparr>tag=Arr T k,values=t\<rparr>"
    1.18 @@ -134,7 +134,7 @@
    1.19  translations
    1.20    "Heap" => "CONST Inl"
    1.21    "Stat" => "CONST Inr"
    1.22 -  "oref" <= (type) "loc + qtname"
    1.23 +  (type) "oref" <= (type) "loc + qtname"
    1.24  
    1.25  definition fields_table :: "prog \<Rightarrow> qtname \<Rightarrow> (fspec \<Rightarrow> field \<Rightarrow> bool)  \<Rightarrow> (fspec, ty) table" where
    1.26   "fields_table G C P 
    1.27 @@ -213,9 +213,9 @@
    1.28          = "(lname, val) table" *) (* defined in Value.thy local variables *)
    1.29  
    1.30  translations
    1.31 - "globs"  <= (type) "(oref , obj) table"
    1.32 - "heap"   <= (type) "(loc  , obj) table"
    1.33 -(*  "locals" <= (type) "(lname, val) table" *)
    1.34 + (type) "globs"  <= (type) "(oref , obj) table"
    1.35 + (type) "heap"   <= (type) "(loc  , obj) table"
    1.36 +(*  (type) "locals" <= (type) "(lname, val) table" *)
    1.37  
    1.38  datatype st = (* pure state, i.e. contents of all variables *)
    1.39           st globs locals
    1.40 @@ -567,10 +567,8 @@
    1.41    state = "abopt \<times> st"          --{* state including abruption information *}
    1.42  
    1.43  translations
    1.44 -  "abopt"       <= (type) "State.abrupt option"
    1.45 -  "abopt"       <= (type) "abrupt option"
    1.46 -  "state"      <= (type) "abopt \<times> State.st"
    1.47 -  "state"      <= (type) "abopt \<times> st"
    1.48 +  (type) "abopt" <= (type) "abrupt option"
    1.49 +  (type) "state" <= (type) "abopt \<times> st"
    1.50  
    1.51  abbreviation
    1.52    Norm :: "st \<Rightarrow> state"