src/HOL/ex/SVC_Oracle.thy
changeset 16417 9bc16273c2d4
parent 12869 f362c0323d92
child 16836 45a3dc4688bc
     1.1 --- a/src/HOL/ex/SVC_Oracle.thy	Fri Jun 17 11:35:35 2005 +0200
     1.2 +++ b/src/HOL/ex/SVC_Oracle.thy	Fri Jun 17 16:12:49 2005 +0200
     1.3 @@ -8,8 +8,8 @@
     1.4  Based upon the work of Søren T. Heilmann
     1.5  *)
     1.6  
     1.7 -theory SVC_Oracle = Main (** + Real??**)
     1.8 -files "svc_funcs.ML":
     1.9 +theory SVC_Oracle imports Main (** + Real??**)
    1.10 +uses "svc_funcs.ML" begin
    1.11  
    1.12  consts
    1.13    (*reserved for the oracle*)