changeset 16417 | 9bc16273c2d4 |
parent 14957 | 0e94a1ccc6ae |
child 19796 | d86e7b1fc472 |
16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
---|---|
4 Copyright 1991 University of Cambridge |
4 Copyright 1991 University of Cambridge |
5 *) |
5 *) |
6 |
6 |
7 header {* First-Order Logic: the 'if' example *} |
7 header {* First-Order Logic: the 'if' example *} |
8 |
8 |
9 theory If = FOL: |
9 theory If imports FOL begin |
10 |
10 |
11 constdefs |
11 constdefs |
12 if :: "[o,o,o]=>o" |
12 if :: "[o,o,o]=>o" |
13 "if(P,Q,R) == P&Q | ~P&R" |
13 "if(P,Q,R) == P&Q | ~P&R" |
14 |
14 |