(* Title: FOL/ex/IffOracle ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1996 University of Cambridge Example of how to declare an oracle *) IffOracle = "declIffOracle" + FOL + oracle mk_iff_oracle end