| changeset 7162 | 8737390d1d0a |
| parent 7144 | 0feee8201d67 |
| child 7237 | 2919daadba91 |
--- a/src/HOL/SVC_Oracle.thy Tue Aug 03 13:08:18 1999 +0200 +++ b/src/HOL/SVC_Oracle.thy Tue Aug 03 13:08:58 1999 +0200 @@ -9,5 +9,10 @@ *) SVC_Oracle = NatBin + (**Real?? + **) + +consts + (*reserved for the oracle*) + iff_keep, iff_unfold :: [bool, bool] => bool + oracle svc_oracle = Svc.oracle end