changeset 20813 | 379ce56e5dc2 |
parent 17388 | 495c799df31d |
child 24470 | 41c81e23c08d |
--- 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