src/HOL/TLA/Memory/MIParameters.thy
author wenzelm
Fri Oct 05 23:58:52 2001 +0200 (2001-10-05)
changeset 11703 6e5de8d4290a
parent 5184 9b8547a9496a
child 17309 c43ed29bd197
permissions -rw-r--r--
tuned;
wenzelm@3807
     1
(*
wenzelm@3807
     2
    File:        MIParameters.thy
wenzelm@3807
     3
    Author:      Stephan Merz
wenzelm@3807
     4
    Copyright:   1997 University of Munich
wenzelm@3807
     5
wenzelm@3807
     6
    Theory Name: MIParameters
wenzelm@3807
     7
    Logic Image: TLA
wenzelm@3807
     8
wenzelm@3807
     9
    RPC-Memory example: Parameters of the memory implementation.
wenzelm@3807
    10
*)
wenzelm@3807
    11
wenzelm@11703
    12
MIParameters = Main +
wenzelm@3807
    13
wenzelm@3807
    14
datatype  histState  =  histA | histB
wenzelm@3807
    15
wenzelm@3807
    16
end