| changeset 48891 | c0eafbd55de3 |
| parent 46218 | ecf6375e2abb |
| child 52131 | 366fa32ee2a3 |
--- a/src/HOL/ex/SVC_Oracle.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/ex/SVC_Oracle.thy Wed Aug 22 22:55:41 2012 +0200 @@ -9,9 +9,10 @@ theory SVC_Oracle imports Main -uses "svc_funcs.ML" begin +ML_file "svc_funcs.ML" + consts iff_keep :: "[bool, bool] => bool" iff_unfold :: "[bool, bool] => bool"