isabelle: src/HOL/TLA/Memory/MemClerkParameters.ML@c43ed29bd197 (annotated)

17309 c43ed29bd197 converted to Isar theory format; wenzelm parents: 6255 diff changeset	1	(*
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	2	File: MemClerkParameters.ML
17309 c43ed29bd197 converted to Isar theory format; wenzelm parents: 6255 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	RPC-Memory example: Memory clerk parameters (ML file)
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
6255 db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	10	(*
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	11	val CP_simps = RP_simps @ mClkState.simps;
6255 db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	12	*)