--- /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);
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOL/ex/IffOracle.thy Tue Mar 05 11:38:41 1996 +0100
@@ -0,0 +1,11 @@
+(* Title: FOL/ex/IffOracle
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1996 University of Cambridge
+
+Example of how to declare an oracle
+*)
+
+IffOracle = "declIffOracle" + FOL +
+oracle mk_iff_oracle
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOL/ex/declIffOracle.ML Tue Mar 05 11:38:41 1996 +0100
@@ -0,0 +1,24 @@
+(* Title: FOL/ex/declIffOracle
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1996 University of Cambridge
+
+Example of how to declare an oracle
+*)
+
+
+(*New exception constructor for passing arguments to the oracle*)
+exception IffOracleExn of int;
+
+(*Internal syntactic declarations*)
+val oT = Type("o",[]);
+
+val iff = Const("op <->", [oT,oT]--->oT);
+
+fun mk_iff 0 = Const("True", oT)
+ | mk_iff n = iff $ Free("P", oT) $ mk_iff (n-1);
+
+val Trueprop = Const("Trueprop",oT-->propT);
+
+(*Oracle makes tautologies of the form "P <-> P <-> P <-> P <-> True"*)
+fun mk_iff_oracle (sign, IffOracleExn n) = Trueprop $ mk_iff (2*n);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOL/ex/declIffOracle.thy Tue Mar 05 11:38:41 1996 +0100
@@ -0,0 +1,1 @@
+declIffOracle = Pure