equal
deleted
inserted
replaced
4 Copyright 1996 University of Cambridge |
4 Copyright 1996 University of Cambridge |
5 *) |
5 *) |
6 |
6 |
7 header{*Example of Declaring an Oracle*} |
7 header{*Example of Declaring an Oracle*} |
8 |
8 |
9 theory IffOracle = FOL: |
9 theory IffOracle imports FOL begin |
10 |
10 |
11 text{*This oracle makes tautologies of the form "P <-> P <-> P <-> P". |
11 text{*This oracle makes tautologies of the form "P <-> P <-> P <-> P". |
12 The length is specified by an integer, which is checked to be even and |
12 The length is specified by an integer, which is checked to be even and |
13 positive.*} |
13 positive.*} |
14 |
14 |