proper use of svc_oracle.ML;
authorwenzelm
Sun, 01 Oct 2006 18:29:32 +0200
changeset 20813 379ce56e5dc2
parent 20812 cc6b31c2b9a2
child 20814 bc3a2b9b9960
proper use of svc_oracle.ML;
src/HOL/ex/SVC_Oracle.thy
--- a/src/HOL/ex/SVC_Oracle.thy	Sun Oct 01 18:29:31 2006 +0200
+++ b/src/HOL/ex/SVC_Oracle.thy	Sun Oct 01 18:29:32 2006 +0200
@@ -10,7 +10,7 @@
 
 theory SVC_Oracle
 imports Main
-uses "svc_funcs.ML"
+uses "svc_funcs.ML" ("svc_oracle.ML")
 begin
 
 consts
@@ -22,4 +22,6 @@
 oracle
   svc_oracle ("term") = Svc.oracle
 
+use "svc_oracle.ML"
+
 end