src/HOL/TLA/Memory/Memory.thy
changeset 42018 878f33040280
parent 41589 bbd861837ebc
child 42769 053b4b487085
     1.1 --- a/src/HOL/TLA/Memory/Memory.thy	Sun Mar 20 22:48:08 2011 +0100
     1.2 +++ b/src/HOL/TLA/Memory/Memory.thy	Sun Mar 20 23:07:06 2011 +0100
     1.3 @@ -8,10 +8,9 @@
     1.4  imports MemoryParameters ProcedureInterface
     1.5  begin
     1.6  
     1.7 -types
     1.8 -  memChType  = "(memOp, Vals) channel"
     1.9 -  memType = "(Locs => Vals) stfun"      (* intention: MemLocs => MemVals *)
    1.10 -  resType = "(PrIds => Vals) stfun"
    1.11 +type_synonym memChType = "(memOp, Vals) channel"
    1.12 +type_synonym memType = "(Locs => Vals) stfun"  (* intention: MemLocs => MemVals *)
    1.13 +type_synonym resType = "(PrIds => Vals) stfun"
    1.14  
    1.15  consts
    1.16    (* state predicates *)