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