--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOL/ex/IffOracle.ML Tue Mar 05 11:38:41 1996 +0100
@@ -0,0 +1,13 @@
+(* Title: FOL/ex/IffOracle
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1996 University of Cambridge
+
+Example of how to use an oracle
+*)
+
+invoke_oracle (IffOracle.thy, sign_of IffOracle.thy, IffOracleExn 0);
+invoke_oracle (IffOracle.thy, sign_of IffOracle.thy, IffOracleExn 5);
+invoke_oracle (IffOracle.thy, sign_of IffOracle.thy, IffOracleExn 10);
+#der(rep_thm it);
+