--- a/src/FOL/IsaMakefile Thu Oct 09 14:56:52 1997 +0200
+++ b/src/FOL/IsaMakefile Thu Oct 09 14:59:36 1997 +0200
@@ -12,7 +12,7 @@
FILES = ROOT.ML IFOL.thy IFOL.ML FOL.thy FOL.ML intprover.ML simpdata.ML \
cladata.ML $(PROVERS:%=../Provers/%)
-EX_NAMES = If List Nat Nat2 Prolog declIffOracle IffOracle
+EX_NAMES = If List Nat Nat2 Prolog IffOracle
EX_FILES = ex/ROOT.ML ex/cla.ML ex/foundn.ML ex/int.ML ex/intro.ML \
ex/prop.ML ex/quant.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
--- a/src/FOL/ex/IffOracle.ML Thu Oct 09 14:56:52 1997 +0200
+++ b/src/FOL/ex/IffOracle.ML Thu Oct 09 14:59:36 1997 +0200
@@ -1,4 +1,4 @@
-(* Title: FOL/ex/IffOracle
+(* Title: FOL/ex/IffOracle.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
@@ -6,14 +6,18 @@
Example of how to use an oracle
*)
-invoke_oracle (IffOracle.thy, sign_of IffOracle.thy, IffOracleExn 2);
-invoke_oracle (IffOracle.thy, sign_of IffOracle.thy, IffOracleExn 10);
+fun iff_oracle n =
+ invoke_oracle IffOracle.thy "iff" (sign_of IffOracle.thy, IffOracleExn n);
+
+
+iff_oracle 2;
+iff_oracle 10;
#der(rep_thm it);
(*These oracle calls had better fail*)
-(invoke_oracle (IffOracle.thy, sign_of IffOracle.thy, IffOracleExn 5);
- raise ERROR) handle IffOracleExn _ => writeln"Failed, as expected";
+(iff_oracle 5; raise ERROR)
+ handle IffOracleExn _ => writeln"Failed, as expected";
-(invoke_oracle (IffOracle.thy, sign_of IffOracle.thy, IffOracleExn 0);
- raise ERROR) handle IffOracleExn _ => writeln"Failed, as expected";
+(iff_oracle 0; raise ERROR)
+ handle IffOracleExn _ => writeln"Failed, as expected";
--- a/src/FOL/ex/IffOracle.thy Thu Oct 09 14:56:52 1997 +0200
+++ b/src/FOL/ex/IffOracle.thy Thu Oct 09 14:59:36 1997 +0200
@@ -1,4 +1,4 @@
-(* Title: FOL/ex/IffOracle
+(* Title: FOL/ex/IffOracle.thy
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
@@ -6,6 +6,38 @@
Example of how to declare an oracle
*)
-IffOracle = "declIffOracle" + FOL +
-oracle mk_iff_oracle
+IffOracle = FOL +
+
+oracle
+ iff = mk_iff_oracle
+
end
+
+
+ML
+
+local
+
+(* internal syntactic declarations *)
+
+val oT = Type("o",[]);
+
+val iff = Const("op <->", [oT,oT]--->oT);
+
+fun mk_iff 1 = Free("P", oT)
+ | mk_iff n = iff $ Free("P", oT) $ mk_iff (n-1);
+
+val Trueprop = Const("Trueprop",oT-->propT);
+
+in
+
+(*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;
--- a/src/FOL/ex/declIffOracle.ML Thu Oct 09 14:56:52 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-(* 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 1 = Free("P", 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"*)
-fun mk_iff_oracle (sign, IffOracleExn n) =
- if n>0 andalso n mod 2 = 0
- then Trueprop $ mk_iff n
- else raise IffOracleExn n;
--- a/src/FOL/ex/declIffOracle.thy Thu Oct 09 14:56:52 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-declIffOracle = Pure