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/MIParameters.thy
author wenzelm
Thu, 10 May 2007 00:39:46 +0200
changeset 22901 481cd919c47f
parent 17309 c43ed29bd197
child 24180 9f818139951b
permissions -rw-r--r--
Thm.first_order_match;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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





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















isabelle