author | paulson |
Tue, 05 Mar 1996 11:38:41 +0100 | |
changeset 1537 | 3f51f0945a3e |
child 1847 | 58ab3b74a344 |
permissions | -rw-r--r-- |
(* Title: FOL/ex/IffOracle ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1996 University of Cambridge Example of how to use an oracle *) invoke_oracle (IffOracle.thy, sign_of IffOracle.thy, IffOracleExn 0); invoke_oracle (IffOracle.thy, sign_of IffOracle.thy, IffOracleExn 5); invoke_oracle (IffOracle.thy, sign_of IffOracle.thy, IffOracleExn 10); #der(rep_thm it);