# HG changeset patch
# User paulson
# Date 1116926390 -7200
# Node ID 7dd4eb2c8055a1d92f6d8dd88d106ee6995a1a81
# Parent  f8110bd9957f8dfa185374e4af7fd0ae9493a51a
oracle example converted to Isar

diff -r f8110bd9957f -r 7dd4eb2c8055 src/FOL/ex/IffOracle.ML
--- a/src/FOL/ex/IffOracle.ML	Tue May 24 10:55:11 2005 +0200
+++ b/src/FOL/ex/IffOracle.ML	Tue May 24 11:19:50 2005 +0200
@@ -6,8 +6,9 @@
 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);
+  invoke_oracle IffOracle_thy "iff" (Theory.sign_of IffOracle_thy, IffOracleExn n);
 
 
 iff_oracle 2;
diff -r f8110bd9957f -r 7dd4eb2c8055 src/FOL/ex/IffOracle.thy
--- a/src/FOL/ex/IffOracle.thy	Tue May 24 10:55:11 2005 +0200
+++ b/src/FOL/ex/IffOracle.thy	Tue May 24 11:19:50 2005 +0200
@@ -2,20 +2,18 @@
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1996  University of Cambridge
-
-Example of how to declare an oracle
 *)
 
-IffOracle = FOL +
+header{*Example of Declaring an Oracle*}
+
+theory IffOracle = FOL:
 
-oracle
-  iff = mk_iff_oracle
-
-end
-
+text{*This oracle makes tautologies of the form "P <-> P <-> P <-> P".
+The length is specified by an integer, which is checked to be even and 
+positive.*}
 
 ML
-
+{*
 local
 
 (* internal syntactic declarations *)
@@ -34,10 +32,17 @@
 (*new exception constructor for passing arguments to the oracle*)
 exception IffOracleExn of int;
 
-(*oracle makes tautologies of the form "P <-> P <-> P <-> P"*)
 fun mk_iff_oracle (sign, IffOracleExn n) =
   if n > 0 andalso n mod 2 = 0
   then Trueprop $ mk_iff n
   else raise IffOracleExn n;
 
-end;
+end
+*}
+
+oracle
+  iff = mk_iff_oracle
+
+end
+
+