--- a/src/HOL/ex/SVC_Oracle.thy Thu Jul 14 19:28:17 2005 +0200
+++ b/src/HOL/ex/SVC_Oracle.thy Thu Jul 14 19:28:18 2005 +0200
@@ -8,15 +8,18 @@
Based upon the work of Søren T. Heilmann
*)
-theory SVC_Oracle imports Main (** + Real??**)
-uses "svc_funcs.ML" begin
+theory SVC_Oracle
+imports Main
+uses "svc_funcs.ML"
+begin
consts
- (*reserved for the oracle*)
iff_keep :: "[bool, bool] => bool"
iff_unfold :: "[bool, bool] => bool"
+hide const iff_keep iff_unfold
+
oracle
- svc_oracle = Svc.oracle
+ svc_oracle ("term") = Svc.oracle
end