| changeset 25946 | 8ceff6c1f2a8 |
| parent 25940 | 6942f3c5dec8 |
| child 27809 | a1e409db516b |
--- a/src/FOL/ex/IffOracle.thy Wed Jan 23 09:57:55 2008 +0100 +++ b/src/FOL/ex/IffOracle.thy Wed Jan 23 22:57:07 2008 +0100 @@ -35,6 +35,7 @@ ML {* iff_oracle @{theory} 2 *} ML {* iff_oracle @{theory} 10 *} +ML {* #der (Thm.rep_thm (iff_oracle @{theory} 10)) *} text {* These oracle calls had better fail. *}