(* 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 = Main + datatype histState = histA | histB end