src/HOL/ex/SVC_Oracle.thy
changeset 16836 45a3dc4688bc
parent 16417 9bc16273c2d4
child 17388 495c799df31d
     1.1 --- a/src/HOL/ex/SVC_Oracle.thy	Thu Jul 14 19:28:17 2005 +0200
     1.2 +++ b/src/HOL/ex/SVC_Oracle.thy	Thu Jul 14 19:28:18 2005 +0200
     1.3 @@ -8,15 +8,18 @@
     1.4  Based upon the work of Søren T. Heilmann
     1.5  *)
     1.6  
     1.7 -theory SVC_Oracle imports Main (** + Real??**)
     1.8 -uses "svc_funcs.ML" begin
     1.9 +theory SVC_Oracle
    1.10 +imports Main
    1.11 +uses "svc_funcs.ML"
    1.12 +begin
    1.13  
    1.14  consts
    1.15 -  (*reserved for the oracle*)
    1.16    iff_keep :: "[bool, bool] => bool"
    1.17    iff_unfold :: "[bool, bool] => bool"
    1.18  
    1.19 +hide const iff_keep iff_unfold
    1.20 +
    1.21  oracle
    1.22 -  svc_oracle = Svc.oracle
    1.23 +  svc_oracle ("term") = Svc.oracle
    1.24  
    1.25  end