Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/TLA/Memory/RPCMemoryParams.thy
author wenzelm
Wed, 08 Oct 1997 11:50:33 +0200
changeset 3807 82a99b090d9d
child 6255 db63752140c7
permissions -rw-r--r--
A formalization of TLA in HOL -- by Stephan Merz;

(* 
    File:        RPCMemoryParams.thy
    Author:      Stephan Merz
    Copyright:   1997 University of Munich

    Theory Name: RPCMemoryParams
    Logic Image: TLA

    Basic declarations for the RPC-memory example.
*)

RPCMemoryParams = HOL +

types
  bit = "bool"   (* signal wires for the procedure interface *)
                 (* Defined as bool for simplicity. All I should really need is *)
                 (* the existence of two distinct values. *)
  Locs           (* "syntactic" value type *)
  Vals           (* "syntactic" value type *)
  PrIds          (* process id's *)

(* all of these are simple (HOL) types *)
arities
  Locs   :: term
  Vals   :: term
  PrIds  :: term

end
isabelle