| changeset 16417 | 9bc16273c2d4 |
| parent 12869 | f362c0323d92 |
| child 16836 | 45a3dc4688bc |
--- a/src/HOL/ex/SVC_Oracle.thy Fri Jun 17 11:35:35 2005 +0200 +++ b/src/HOL/ex/SVC_Oracle.thy Fri Jun 17 16:12:49 2005 +0200 @@ -8,8 +8,8 @@ Based upon the work of Søren T. Heilmann *) -theory SVC_Oracle = Main (** + Real??**) -files "svc_funcs.ML": +theory SVC_Oracle imports Main (** + Real??**) +uses "svc_funcs.ML" begin consts (*reserved for the oracle*)