src/HOL/IMP/Com.thy
changeset 42174 d0be2722ce9f
parent 41589 bbd861837ebc
child 43141 11fce8564415
     1.1 --- a/src/HOL/IMP/Com.thy	Wed Mar 30 22:53:18 2011 +0200
     1.2 +++ b/src/HOL/IMP/Com.thy	Wed Mar 30 23:26:40 2011 +0200
     1.3 @@ -11,11 +11,10 @@
     1.4    -- "an unspecified (arbitrary) type of locations 
     1.5        (adresses/names) for variables"
     1.6        
     1.7 -types 
     1.8 -  val   = nat -- "or anything else, @{text nat} used in examples"
     1.9 -  state = "loc \<Rightarrow> val"
    1.10 -  aexp  = "state \<Rightarrow> val"  
    1.11 -  bexp  = "state \<Rightarrow> bool"
    1.12 +type_synonym val = nat -- "or anything else, @{text nat} used in examples"
    1.13 +type_synonym state = "loc \<Rightarrow> val"
    1.14 +type_synonym aexp = "state \<Rightarrow> val"
    1.15 +type_synonym bexp = "state \<Rightarrow> bool"
    1.16    -- "arithmetic and boolean expressions are not modelled explicitly here,"
    1.17    -- "they are just functions on states"
    1.18