| changeset 346 | 0fea8b7a14a1 |
| parent 211 | d5accbc67e1b |
| child 457 | aedfdcae39a9 |
| 345:4c54ef4dc84d | 346:0fea8b7a14a1 |
|---|---|
1 theory Oracle |
1 theory Oracle |
2 imports "../Base" |
2 imports "../Appendix" |
3 uses ("external_solver.ML") |
3 uses ("external_solver.ML") |
4 begin |
4 begin |
5 |
5 |
6 section {* Writing an Oracle (TBD)\label{rec:oracle} *} |
6 section {* Writing an Oracle (TBD)\label{rec:oracle} *} |
7 |
7 |