author | wenzelm |
Wed, 23 Jan 2008 22:57:07 +0100 | |
changeset 25946 | 8ceff6c1f2a8 |
parent 25945 | ddc6a3312636 |
child 25947 | 1f2f4d941e9e |
--- 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. *}