src/FOL/ex/IffOracle.ML

Put in minimal simpset to avoid excessive simplification,
just as in revision 1.9 of HOL/indrule.ML

(*  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 2);
invoke_oracle (IffOracle.thy, sign_of IffOracle.thy, IffOracleExn 10);
#der(rep_thm it);

(*These oracle calls had better fail*)

(invoke_oracle (IffOracle.thy, sign_of IffOracle.thy, IffOracleExn 5); 
 raise ERROR) handle IffOracleExn _ => writeln"Failed, as expected";  

(invoke_oracle (IffOracle.thy, sign_of IffOracle.thy, IffOracleExn 0); 
 raise ERROR) handle IffOracleExn _ => writeln"Failed, as expected";