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 = Main (** + Real??**) |
11 theory SVC_Oracle imports Main (** + Real??**) |
12 files "svc_funcs.ML": |
12 uses "svc_funcs.ML" begin |
13 |
13 |
14 consts |
14 consts |
15 (*reserved for the oracle*) |
15 (*reserved for the oracle*) |
16 iff_keep :: "[bool, bool] => bool" |
16 iff_keep :: "[bool, bool] => bool" |
17 iff_unfold :: "[bool, bool] => bool" |
17 iff_unfold :: "[bool, bool] => bool" |