src/HOL/TLA/Memory/MemClerkParameters.thy
changeset 21624 6f79647cf536
parent 17309 c43ed29bd197
child 36866 426d5781bb25
     1.1 --- a/src/HOL/TLA/Memory/MemClerkParameters.thy	Fri Dec 01 17:22:33 2006 +0100
     1.2 +++ b/src/HOL/TLA/Memory/MemClerkParameters.thy	Sat Dec 02 02:52:02 2006 +0100
     1.3 @@ -3,12 +3,9 @@
     1.4      ID:          $Id$
     1.5      Author:      Stephan Merz
     1.6      Copyright:   1997 University of Munich
     1.7 +*)
     1.8  
     1.9 -    Theory Name: MemClerkParameters
    1.10 -    Logic Image: TLA
    1.11 -
    1.12 -    RPC-Memory example: Parameters of the memory clerk.
    1.13 -*)
    1.14 +header {* RPC-Memory example: Parameters of the memory clerk *}
    1.15  
    1.16  theory MemClerkParameters
    1.17  imports RPCParameters
    1.18 @@ -30,6 +27,4 @@
    1.19    MClkReplyVal     :: "Vals => Vals"
    1.20      "MClkReplyVal v == if v = RPCFailure then MemFailure else v"
    1.21  
    1.22 -ML {* use_legacy_bindings (the_context ()) *}
    1.23 -
    1.24  end