--- a/ProgTutorial/Recipes/Oracle.thy Mon Oct 12 17:07:17 2009 +0200 +++ b/ProgTutorial/Recipes/Oracle.thy Tue Oct 13 22:57:25 2009 +0200 @@ -1,5 +1,5 @@ theory Oracle -imports "../Base" +imports "../Appendix" uses ("external_solver.ML") begin