author | wenzelm |
Sat, 21 Nov 1998 12:17:18 +0100 | |
changeset 5944 | dcc446da8e19 |
parent 3817 | f20f193d42b4 |
child 6391 | 0da748358eff |
permissions | -rw-r--r-- |
3817 | 1 |
(* Title: FOL/ex/IffOracle.ML |
1537 | 2 |
ID: $Id$ |
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1996 University of Cambridge |
|
5 |
||
6 |
Example of how to use an oracle |
|
7 |
*) |
|
8 |
||
3817 | 9 |
fun iff_oracle n = |
10 |
invoke_oracle IffOracle.thy "iff" (sign_of IffOracle.thy, IffOracleExn n); |
|
11 |
||
12 |
||
13 |
iff_oracle 2; |
|
14 |
iff_oracle 10; |
|
1537 | 15 |
#der(rep_thm it); |
16 |
||
1847
58ab3b74a344
Modified to reject certain inputs -- illustrates error handling
paulson
parents:
1537
diff
changeset
|
17 |
(*These oracle calls had better fail*) |
58ab3b74a344
Modified to reject certain inputs -- illustrates error handling
paulson
parents:
1537
diff
changeset
|
18 |
|
3817 | 19 |
(iff_oracle 5; raise ERROR) |
20 |
handle IffOracleExn _ => writeln"Failed, as expected"; |
|
1847
58ab3b74a344
Modified to reject certain inputs -- illustrates error handling
paulson
parents:
1537
diff
changeset
|
21 |
|
3817 | 22 |
(iff_oracle 0; raise ERROR) |
23 |
handle IffOracleExn _ => writeln"Failed, as expected"; |