src/HOL/ex/SVC_Oracle.thy
changeset 20813 379ce56e5dc2
parent 17388 495c799df31d
child 24470 41c81e23c08d
equal deleted inserted replaced
20812:cc6b31c2b9a2 20813:379ce56e5dc2
     8 
     8 
     9 header {* Installing an oracle for SVC (Stanford Validity Checker) *}
     9 header {* Installing an oracle for SVC (Stanford Validity Checker) *}
    10 
    10 
    11 theory SVC_Oracle
    11 theory SVC_Oracle
    12 imports Main
    12 imports Main
    13 uses "svc_funcs.ML"
    13 uses "svc_funcs.ML" ("svc_oracle.ML")
    14 begin
    14 begin
    15 
    15 
    16 consts
    16 consts
    17   iff_keep :: "[bool, bool] => bool"
    17   iff_keep :: "[bool, bool] => bool"
    18   iff_unfold :: "[bool, bool] => bool"
    18   iff_unfold :: "[bool, bool] => bool"
    20 hide const iff_keep iff_unfold
    20 hide const iff_keep iff_unfold
    21 
    21 
    22 oracle
    22 oracle
    23   svc_oracle ("term") = Svc.oracle
    23   svc_oracle ("term") = Svc.oracle
    24 
    24 
       
    25 use "svc_oracle.ML"
       
    26 
    25 end
    27 end