equal
deleted
inserted
replaced
2 imports "../Base" |
2 imports "../Base" |
3 uses ("external_solver.ML") |
3 uses ("external_solver.ML") |
4 begin |
4 begin |
5 |
5 |
6 |
6 |
7 section {* Executing an External Application *} |
7 section {* Executing an External Application \label{rec:external}*} |
8 |
8 |
9 text {* |
9 text {* |
10 {\bf Problem:} |
10 {\bf Problem:} |
11 You want to use an external application. |
11 You want to use an external application. |
12 \smallskip |
12 \smallskip |
55 |
55 |
56 |
56 |
57 |
57 |
58 |
58 |
59 |
59 |
60 section {* Writing an Oracle\label{rec:external} *} |
60 section {* Writing an Oracle\label{rec:oracle} *} |
61 |
61 |
62 text {* |
62 text {* |
|
63 (FIXME: should go into a separate file) |
|
64 |
63 {\bf Problem:} |
65 {\bf Problem:} |
64 You want to use a fast, new decision procedure not based one Isabelle's |
66 You want to use a fast, new decision procedure not based one Isabelle's |
65 tactics, and you do not care whether it is sound. |
67 tactics, and you do not care whether it is sound. |
66 \smallskip |
68 \smallskip |
67 |
69 |