131 text {*

   131 text {*

   132   and create a new method solely based on this tactic:

   132   and create a new method solely based on this tactic:

   133 *}

   133 *}

   134 

   134 

   135 method_setup iff_oracle = {*

   135 method_setup iff_oracle = {*

   137 *} "Oracle-based decision procedure for chains of equivalences"

   137 *} "Oracle-based decision procedure for chains of equivalences"

   138 

   138 

   139 text {*

   139 text {*

   142   Finally, we can test our oracle to prove some theorems:

   140   Finally, we can test our oracle to prove some theorems:

   143 *}

   141 *}

   144 

   142 

   145 lemma "p = (p::bool)"

   143 lemma "p = (p::bool)"

   146    by iff_oracle

   144    by iff_oracle