isabelle: src/HOL/TLA/Memory/MIParameters.thy@c43ed29bd197 (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
17309 c43ed29bd197 converted to Isar theory format; wenzelm parents: 11703 diff changeset	3	ID: $Id$
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	4	Author: Stephan Merz
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	5	Copyright: 1997 University of Munich
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	6
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	7	Theory Name: MIParameters
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	8	Logic Image: TLA
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	9
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	10	RPC-Memory example: Parameters of the memory implementation.
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	11	*)
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	12
11703 6e5de8d4290a tuned; wenzelm parents: 5184 diff changeset	13	MIParameters = Main +
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	14
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	15	datatype histState = histA \| histB
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	16
17309 c43ed29bd197 converted to Isar theory format; wenzelm parents: 11703 diff changeset	17	ML {* use_legacy_bindings (the_context ()) *}
c43ed29bd197 converted to Isar theory format; wenzelm parents: 11703 diff changeset	18
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	19	end

author	wenzelm
	Wed, 07 Sep 2005 20:22:39 +0200
changeset 17309	c43ed29bd197
parent 11703	6e5de8d4290a
child 24180	9f818139951b
permissions	-rw-r--r--