author | wenzelm |
Mon, 08 Feb 1999 13:02:56 +0100 | |
changeset 6255 | db63752140c7 |
parent 3807 | 82a99b090d9d |
child 9517 | f58863b1406a |
permissions | -rw-r--r-- |
(* File: RPCParameters.ML Author: Stephan Merz Copyright: 1997 University of Munich RPC-Memory example: RPC parameters (theorems and proofs) *) (* val RP_simps = MP_simps @ [RFNoMemVal, NotAResultNotRF, OKNotRF, BANotRF] @ (map (fn x => x RS not_sym) [NotAResultNotRF, OKNotRF, BANotRF]) @ rpcState.simps @ rpcOp.simps; *) Addsimps ([RFNoMemVal, NotAResultNotRF, OKNotRF, BANotRF] @ (map (fn x => x RS not_sym) [NotAResultNotRF, OKNotRF, BANotRF]));