equal
deleted
inserted
replaced
1 theory Oracle |
1 theory Oracle |
2 imports "../Base" |
2 imports "../Base" |
3 uses ("external_solver.ML") |
3 uses ("external_solver.ML") |
4 begin |
4 begin |
5 |
5 |
6 section {* Writing an Oracle\label{rec:oracle} *} |
6 section {* Writing an Oracle (TBD)\label{rec:oracle} *} |
7 |
7 |
8 text {* |
8 text {* |
9 {\bf Problem:} |
9 {\bf Problem:} |
10 You want to use a fast, new decision procedure not based one Isabelle's |
10 You want to use a fast, new decision procedure not based one Isabelle's |
11 tactics, and you do not care whether it is sound. |
11 tactics, and you do not care whether it is sound. |