changeset 1537 | 3f51f0945a3e |
child 3817 | f20f193d42b4 |
1536:efbc887dfefb | 1537:3f51f0945a3e |
---|---|
1 (* Title: FOL/ex/IffOracle |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1996 University of Cambridge |
|
5 |
|
6 Example of how to declare an oracle |
|
7 *) |
|
8 |
|
9 IffOracle = "declIffOracle" + FOL + |
|
10 oracle mk_iff_oracle |
|
11 end |