# HG changeset patch
# User wenzelm
# Date 1121362092 -7200
# Node ID 5a2a600e00630f38e008910d913c3f3c639429bc
# Parent  9a6131627ea38f92d4cf4cc117e45504e143ff0b
obsolete;

diff -r 9a6131627ea3 -r 5a2a600e0063 src/FOL/ex/IffOracle.ML
--- a/src/FOL/ex/IffOracle.ML	Thu Jul 14 19:28:12 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-(*  Title:      FOL/ex/IffOracle.ML
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1996  University of Cambridge
-
-Example of how to use an oracle
-*)
-
-val IffOracle_thy = the_context ();
-fun iff_oracle n =
-  invoke_oracle IffOracle_thy "iff" (Theory.sign_of IffOracle_thy, IffOracleExn n);
-
-
-iff_oracle 2;
-iff_oracle 10;
-#der(rep_thm it);
-
-(*These oracle calls had better fail*)
-
-(iff_oracle 5; raise ERROR)
-  handle IffOracleExn _ => writeln"Failed, as expected";
-
-(iff_oracle 0; raise ERROR)
-  handle IffOracleExn _ => writeln"Failed, as expected";