Mercurial Mercurial > repos > isabelle / annotate
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
Sun, 30 Jan 2011 13:02:18 +0100
changeset 41648 6d736d983d5c
parent 41589 bbd861837ebc
child 42018 878f33040280
permissions -rw-r--r--
clarified example settings for Proof General;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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














82a99b090d9d
A formalization of TLA in HOL -- by Stephan Merz;



wenzelm


parents: 

diff
changeset




    11


types








6255






db63752140c7
updated (Stephan Merz);



wenzelm


parents: 
3807

diff
changeset




    12


  bit = "bool"   (* Signal wires for the procedure interface.













db63752140c7
updated (Stephan Merz);



wenzelm


parents: 
3807

diff
changeset




    13


                    Defined as bool for simplicity. All I should really need is













db63752140c7
updated (Stephan Merz);



wenzelm


parents: 
3807

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





wenzelm


parents: 
6255

diff
changeset




    17


typedecl Locs    (* "syntactic" value type *)












wenzelm


parents: 
6255

diff
changeset




    18


typedecl Vals    (* "syntactic" value type *)












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















isabelle