recovered #der example without using val it;
authorwenzelm
Wed, 23 Jan 2008 22:57:07 +0100
changeset 25946 8ceff6c1f2a8
parent 25945 ddc6a3312636
child 25947 1f2f4d941e9e
recovered #der example without using val it;
src/FOL/ex/IffOracle.thy
--- 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. *}