src/HOL/TLA/Memory/RPCParameters.ML
author wenzelm
Thu Mar 11 13:20:35 1999 +0100 (1999-03-11)
changeset 6349 f7750d816c21
parent 6255 db63752140c7
child 9517 f58863b1406a
permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
wenzelm@3807
     1
(* 
wenzelm@3807
     2
    File:        RPCParameters.ML
wenzelm@3807
     3
    Author:      Stephan Merz
wenzelm@3807
     4
    Copyright:   1997 University of Munich
wenzelm@3807
     5
wenzelm@6255
     6
    RPC-Memory example: RPC parameters (theorems and proofs)
wenzelm@3807
     7
*)
wenzelm@3807
     8
wenzelm@3807
     9
wenzelm@6255
    10
(*
wenzelm@3807
    11
val RP_simps = MP_simps @ [RFNoMemVal, NotAResultNotRF, OKNotRF, BANotRF]
wenzelm@3807
    12
                        @ (map (fn x => x RS not_sym) [NotAResultNotRF, OKNotRF, BANotRF])
wenzelm@6255
    13
                        @ rpcState.simps @ rpcOp.simps;
wenzelm@6255
    14
*)
wenzelm@6255
    15
wenzelm@6255
    16
Addsimps ([RFNoMemVal, NotAResultNotRF, OKNotRF, BANotRF]
wenzelm@6255
    17
          @ (map (fn x => x RS not_sym) [NotAResultNotRF, OKNotRF, BANotRF]));