proper use of svc_oracle.ML;
authorwenzelm
Sun Oct 01 18:29:32 2006 +0200 (2006-10-01)
changeset 20813379ce56e5dc2
parent 20812 cc6b31c2b9a2
child 20814 bc3a2b9b9960
proper use of svc_oracle.ML;
src/HOL/ex/SVC_Oracle.thy
     1.1 --- a/src/HOL/ex/SVC_Oracle.thy	Sun Oct 01 18:29:31 2006 +0200
     1.2 +++ b/src/HOL/ex/SVC_Oracle.thy	Sun Oct 01 18:29:32 2006 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4  
     1.5  theory SVC_Oracle
     1.6  imports Main
     1.7 -uses "svc_funcs.ML"
     1.8 +uses "svc_funcs.ML" ("svc_oracle.ML")
     1.9  begin
    1.10  
    1.11  consts
    1.12 @@ -22,4 +22,6 @@
    1.13  oracle
    1.14    svc_oracle ("term") = Svc.oracle
    1.15  
    1.16 +use "svc_oracle.ML"
    1.17 +
    1.18  end