equal
deleted
inserted
replaced
5 *) |
5 *) |
6 |
6 |
7 header {* Evaluation Oracle with ML witnesses *} |
7 header {* Evaluation Oracle with ML witnesses *} |
8 |
8 |
9 theory Eval_Witness |
9 theory Eval_Witness |
10 imports Plain List |
10 imports Plain "~~/src/HOL/List" |
11 begin |
11 begin |
12 |
12 |
13 text {* |
13 text {* |
14 We provide an oracle method similar to "eval", but with the |
14 We provide an oracle method similar to "eval", but with the |
15 possibility to provide ML values as witnesses for existential |
15 possibility to provide ML values as witnesses for existential |