src/HOL/ex/SVC_Oracle.thy
changeset 16836 45a3dc4688bc
parent 16417 9bc16273c2d4
child 17388 495c799df31d
--- 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