recovered #der example without using val it;
authorwenzelm
Wed Jan 23 22:57:07 2008 +0100 (2008-01-23)
changeset 259468ceff6c1f2a8
parent 25945 ddc6a3312636
child 25947 1f2f4d941e9e
recovered #der example without using val it;
src/FOL/ex/IffOracle.thy
     1.1 --- a/src/FOL/ex/IffOracle.thy	Wed Jan 23 09:57:55 2008 +0100
     1.2 +++ b/src/FOL/ex/IffOracle.thy	Wed Jan 23 22:57:07 2008 +0100
     1.3 @@ -35,6 +35,7 @@
     1.4  
     1.5  ML {* iff_oracle @{theory} 2 *}
     1.6  ML {* iff_oracle @{theory} 10 *}
     1.7 +ML {* #der (Thm.rep_thm (iff_oracle @{theory} 10)) *}
     1.8  
     1.9  text {* These oracle calls had better fail. *}
    1.10