src/HOL/TLA/Memory/MIParameters.thy
changeset 3807 82a99b090d9d
child 5184 9b8547a9496a
equal deleted inserted replaced
3806:f371115aed37 3807:82a99b090d9d
       
     1 (*
       
     2     File:        MIParameters.thy
       
     3     Author:      Stephan Merz
       
     4     Copyright:   1997 University of Munich
       
     5 
       
     6     Theory Name: MIParameters
       
     7     Logic Image: TLA
       
     8 
       
     9     RPC-Memory example: Parameters of the memory implementation.
       
    10 *)
       
    11 
       
    12 MIParameters = Arith +
       
    13 
       
    14 datatype  histState  =  histA | histB
       
    15 
       
    16 end
       
    17