author | wenzelm |
Sat, 01 Dec 2001 18:52:32 +0100 | |
changeset 12338 | de0f4a63baa5 |
parent 9517 | f58863b1406a |
child 17309 | c43ed29bd197 |
permissions | -rw-r--r-- |
3807 | 1 |
(* |
2 |
File: RPCParameters.ML |
|
3 |
Author: Stephan Merz |
|
4 |
Copyright: 1997 University of Munich |
|
5 |
||
6255 | 6 |
RPC-Memory example: RPC parameters (theorems and proofs) |
3807 | 7 |
*) |
8 |
||
9 |
||
6255 | 10 |
Addsimps ([RFNoMemVal, NotAResultNotRF, OKNotRF, BANotRF] |
11 |
@ (map (fn x => x RS not_sym) [NotAResultNotRF, OKNotRF, BANotRF])); |