author | wenzelm |
Sun, 01 Oct 2006 18:29:32 +0200 | |
changeset 20813 | 379ce56e5dc2 |
parent 20812 | cc6b31c2b9a2 |
child 20814 | bc3a2b9b9960 |
--- 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