isabelle: src/HOL/TLA/Memory/MIParameters.thy@a901bafe4578 (annotated)

3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	1	(*
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	2	File: MIParameters.thy
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	3	Author: Stephan Merz
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	4	Copyright: 1997 University of Munich
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	5
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	6	Theory Name: MIParameters
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	7	Logic Image: TLA
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	8
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	9	RPC-Memory example: Parameters of the memory implementation.
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	10	*)
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	11
5184 9b8547a9496a Adapted to new datatype package. berghofe parents: 3807 diff changeset	12	MIParameters = Datatype +
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	13
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	14	datatype histState = histA \| histB
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	15
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	16	end
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	17

author	wenzelm
	Mon, 29 Nov 1999 15:52:49 +0100
changeset 8039	a901bafe4578
parent 5184	9b8547a9496a
child 11703	6e5de8d4290a
permissions	-rw-r--r--