equal
deleted
inserted
replaced
1 (* |
1 (* |
2 File: RPCParameters.ML |
2 File: RPCParameters.ML |
|
3 ID: $Id$ |
3 Author: Stephan Merz |
4 Author: Stephan Merz |
4 Copyright: 1997 University of Munich |
5 Copyright: 1997 University of Munich |
5 |
6 |
6 RPC-Memory example: RPC parameters (theorems and proofs) |
7 RPC-Memory example: RPC parameters (theorems and proofs) |
7 *) |
8 *) |
8 |
9 |
9 |
|
10 Addsimps ([RFNoMemVal, NotAResultNotRF, OKNotRF, BANotRF] |
10 Addsimps ([RFNoMemVal, NotAResultNotRF, OKNotRF, BANotRF] |
11 @ (map (fn x => x RS not_sym) [NotAResultNotRF, OKNotRF, BANotRF])); |
11 @ (map (fn x => x RS not_sym) [NotAResultNotRF, OKNotRF, BANotRF])); |