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 The following code merely CALLS the oracle; |
8 The following code merely CALLS the oracle; |
9 the soundness-critical functions are at HOL/Tools/svc_funcs.ML |
9 the soundness-critical functions are at HOL/Tools/svc_funcs.ML |
10 |
10 |
11 Based upon the work of Søren T. Heilmann |
11 Based upon the work of Soren T. Heilmann |
12 *) |
12 *) |
13 |
13 |
14 |
14 |
15 (*Generalize an Isabelle formula, replacing by Vars |
15 (*Generalize an Isabelle formula, replacing by Vars |
16 all subterms not intelligible to SVC.*) |
16 all subterms not intelligible to SVC.*) |