--- a/CookBook/Recipes/Oracle.thy Tue Mar 17 01:56:29 2009 +0100
+++ b/CookBook/Recipes/Oracle.thy Tue Mar 17 11:47:01 2009 +0100
@@ -133,12 +133,10 @@
*}
method_setup iff_oracle = {*
- Method.no_args (Method.SIMPLE_METHOD' iff_oracle_tac)
+ Scan.succeed (K (Method.SIMPLE_METHOD' iff_oracle_tac))
*} "Oracle-based decision procedure for chains of equivalences"
text {*
- (FIXME: what does @{ML "Method.SIMPLE_METHOD'"} do? ... what do you mean?)
-
Finally, we can test our oracle to prove some theorems:
*}