equal
deleted
inserted
replaced
7 |
7 |
8 header {* Installing an oracle for SVC (Stanford Validity Checker) *} |
8 header {* Installing an oracle for SVC (Stanford Validity Checker) *} |
9 |
9 |
10 theory SVC_Oracle |
10 theory SVC_Oracle |
11 imports Main |
11 imports Main |
12 uses "svc_funcs.ML" |
|
13 begin |
12 begin |
|
13 |
|
14 ML_file "svc_funcs.ML" |
14 |
15 |
15 consts |
16 consts |
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 |