equal
deleted
inserted
replaced
7 *) |
7 *) |
8 |
8 |
9 theory If imports FOL begin |
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 |
15 lemma ifI: |
15 lemma ifI: |
16 "[| P ==> Q; ~P ==> R |] ==> if(P,Q,R)" |
16 "[| P ==> Q; ~P ==> R |] ==> if(P,Q,R)" |
17 --{* @{subgoals[display,indent=0,margin=65]} *} |
17 --{* @{subgoals[display,indent=0,margin=65]} *} |
18 apply (simp add: if_def) |
18 apply (simp add: if_def) |