isabelle: src/HOL/TLA/Memory/RPCMemoryParams.thy@1253fd12ca8a (annotated)

41589 bbd861837ebc tuned headers; wenzelm parents: 21624 diff changeset	1	(* Title: HOL/TLA/Memory/RPCMemoryParams.thy
bbd861837ebc tuned headers; wenzelm parents: 21624 diff changeset	2	Author: Stephan Merz, University of Munich
21624 6f79647cf536 TLA: converted legacy ML scripts; wenzelm parents: 17309 diff changeset	3	*)
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	4
21624 6f79647cf536 TLA: converted legacy ML scripts; wenzelm parents: 17309 diff changeset	5	header {* Basic declarations for the RPC-memory example *}
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	6
17309 c43ed29bd197 converted to Isar theory format; wenzelm parents: 16417 diff changeset	7	theory RPCMemoryParams
c43ed29bd197 converted to Isar theory format; wenzelm parents: 16417 diff changeset	8	imports Main
c43ed29bd197 converted to Isar theory format; wenzelm parents: 16417 diff changeset	9	begin
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	10
42018 878f33040280 modernized specifications; wenzelm parents: 41589 diff changeset	11	type_synonym bit = "bool"
878f33040280 modernized specifications; wenzelm parents: 41589 diff changeset	12	(* Signal wires for the procedure interface.
878f33040280 modernized specifications; wenzelm parents: 41589 diff changeset	13	Defined as bool for simplicity. All I should really need is
878f33040280 modernized specifications; wenzelm parents: 41589 diff changeset	14	the existence of two distinct values. *)
3807 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	(* all of these are simple (HOL) types *)
11703 6e5de8d4290a tuned; wenzelm parents: 6255 diff changeset	17	typedecl Locs (* "syntactic" value type *)
6e5de8d4290a tuned; wenzelm parents: 6255 diff changeset	18	typedecl Vals (* "syntactic" value type *)
6e5de8d4290a tuned; wenzelm parents: 6255 diff changeset	19	typedecl PrIds (* process id's *)
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	20
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	21	end

author	wenzelm
	Sun, 06 Jan 2013 12:44:45 +0100
changeset 50753	1253fd12ca8a
parent 42018	878f33040280
child 58889	5b7a9633cfa8
permissions	-rw-r--r--