src/HOL/ex/SVC_Oracle.thy
changeset 20813 379ce56e5dc2
parent 17388 495c799df31d
child 24470 41c81e23c08d
     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