(* File: MIParameters.thy Author: Stephan Merz Copyright: 1997 University of Munich Theory Name: MIParameters Logic Image: TLA RPC-Memory example: Parameters of the memory implementation. *) MIParameters = Datatype + datatype histState = histA | histB end