equal
deleted
inserted
replaced
6 Installing the oracle for SVC (Stanford Validity Checker) |
6 Installing the oracle for SVC (Stanford Validity Checker) |
7 |
7 |
8 Based upon the work of Søren T. Heilmann |
8 Based upon the work of Søren T. Heilmann |
9 *) |
9 *) |
10 |
10 |
11 theory SVC_Oracle imports Main (** + Real??**) |
11 theory SVC_Oracle |
12 uses "svc_funcs.ML" begin |
12 imports Main |
|
13 uses "svc_funcs.ML" |
|
14 begin |
13 |
15 |
14 consts |
16 consts |
15 (*reserved for the oracle*) |
|
16 iff_keep :: "[bool, bool] => bool" |
17 iff_keep :: "[bool, bool] => bool" |
17 iff_unfold :: "[bool, bool] => bool" |
18 iff_unfold :: "[bool, bool] => bool" |
18 |
19 |
|
20 hide const iff_keep iff_unfold |
|
21 |
19 oracle |
22 oracle |
20 svc_oracle = Svc.oracle |
23 svc_oracle ("term") = Svc.oracle |
21 |
24 |
22 end |
25 end |