changeset 58860 | fee7cfa69c50 |
parent 55380 | 4de48353034e |
child 58889 | 5b7a9633cfa8 |
--- a/src/Sequents/LK0.thy Sat Nov 01 11:40:55 2014 +0100 +++ b/src/Sequents/LK0.thy Sat Nov 01 14:20:38 2014 +0100 @@ -359,7 +359,7 @@ apply fast done -lemma if_not_P: "|- ~P ==> |- (if P then x else y) = y"; +lemma if_not_P: "|- ~P ==> |- (if P then x else y) = y" apply (unfold If_def) apply (erule thinR [THEN cut]) apply fast