equal
deleted
inserted
replaced
6 First-Order Logic: the 'if' example. |
6 First-Order Logic: the 'if' example. |
7 *) |
7 *) |
8 |
8 |
9 theory If imports FOL begin |
9 theory If imports FOL begin |
10 |
10 |
11 constdefs |
11 definition "if" :: "[o,o,o]=>o" where |
12 "if" :: "[o,o,o]=>o" |
|
13 "if(P,Q,R) == P&Q | ~P&R" |
12 "if(P,Q,R) == P&Q | ~P&R" |
14 |
13 |
15 lemma ifI: |
14 lemma ifI: |
16 "[| P ==> Q; ~P ==> R |] ==> if(P,Q,R)" |
15 "[| P ==> Q; ~P ==> R |] ==> if(P,Q,R)" |
17 --{* @{subgoals[display,indent=0,margin=65]} *} |
16 --{* @{subgoals[display,indent=0,margin=65]} *} |