| author | paulson |
| Mon, 20 Mar 2000 12:54:31 +0100 | |
| changeset 8527 | ce6ae118b6b2 |
| parent 6391 | 0da748358eff |
| child 16063 | 7dd4eb2c8055 |
| 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 = |
| 6391 | 10 |
invoke_oracle IffOracle.thy "iff" (Theory.sign_of IffOracle.thy, IffOracleExn n); |
| 3817 | 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"; |