author | wenzelm |
Fri, 05 May 2006 21:59:41 +0200 | |
changeset 19573 | 340c466c9605 |
parent 17309 | c43ed29bd197 |
permissions | -rw-r--r-- |
17309 | 1 |
(* |
3807 | 2 |
File: MemoryParameters.ML |
17309 | 3 |
ID: $Id$ |
3807 | 4 |
Author: Stephan Merz |
5 |
Copyright: 1997 University of Munich |
|
6 |
||
7 |
RPC-Memory example: memory parameters (ML file) |
|
8 |
*) |
|
9 |
||
6255 | 10 |
Addsimps ([BadArgNoMemVal,MemFailNoMemVal,InitValMemVal,NotAResultNotVal, |
11 |
NotAResultNotOK, NotAResultNotBA, NotAResultNotMF] |
|
17309 | 12 |
@ (map (fn x => x RS not_sym) |
6255 | 13 |
[NotAResultNotOK, NotAResultNotBA, NotAResultNotMF])); |
3807 | 14 |
|
17309 | 15 |
val prems = goal (the_context ()) "[| x : MemVal; (x ~= NotAResult ==> P) |] ==> P"; |
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
16 |
by (resolve_tac prems 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
17 |
by (cut_facts_tac (NotAResultNotVal::prems) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
18 |
by (Force_tac 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
19 |
qed "MemValNotAResultE"; |