fixed not-e

[helm.git] / helm / software / matita / library / didactic / support / natural_deduction.ma

diff --git a/helm/software/matita/library/didactic/support/natural_deduction.ma b/helm/software/matita/library/didactic/support/natural_deduction.ma
index 99e047a9dcf64d2d42b5c5b0c26ec0aae4eb7b96..b7ee07cb6da8135c294a57e32a1c9275826383c4 100644 (file)
--- a/helm/software/matita/library/didactic/support/natural_deduction.ma
+++ b/helm/software/matita/library/didactic/support/natural_deduction.ma
@@ -97,19 +97,19 @@ definition show : ∀A.A→A ≝ λA:CProp.λa:A.a.
 (* When something does not fit, this daemon is used *)
 axiom cast: ∀A,B:CProp.B → A.
 
+(* begin a proof: draws the root *)
+notation > "'prove' p" non associative with precedence 19 
+for @{ 'prove $p }.
+interpretation "prove KO" 'prove p = (cast _ _ (show p _)).
+interpretation "prove OK" 'prove p = (show p _).
+
 (* Leaves *)
 notation < "\infrule (t\atop ⋮) a ?" with precedence 19
 for @{ 'leaf_ok $a $t }.
 interpretation "leaf OK" 'leaf_ok a t = (show a t).
 notation < "\infrule (t\atop ⋮) mstyle color #ff0000 (a) ?" with precedence 19 
 for @{ 'leaf_ko $a $t }.
-interpretation "leaf KO" 'leaf_ko a t = (cast _ a (show _ t)).
-
-(* begin a proof: draws the root *)
-notation > "'prove' p" non associative with precedence 19 
-for @{ 'prove $p }.
-interpretation "prove KO" 'prove p = (cast _ _ (show p _)).
-interpretation "prove OK" 'prove p = (show p _).
+interpretation "leaf KO" 'leaf_ko a t = (cast _ _ (show a t)).
 
 (* discharging *)
 notation < "[ a ] \sup mstyle color #ff0000 (H)" with precedence 19 
@@ -430,12 +430,12 @@ interpretation "Not_intro OK" 'Not_intro a = (Not_intro _ a).
 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b mstyle color #ff0000 (\lnot\sub\e) " with precedence 19 
 for @{ 'Not_elim_ko_1 $ab $a $b }.
 interpretation "Not_elim_ko_1" 'Not_elim_ko_1 ab a b = 
-  (show b (cast _ _ (Not_elim _ (cast _ _ ab) a))).
+  (show b (cast _ _ (Not_elim _ (cast _ _ ab) (cast _ _ a)))).
 
 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) mstyle color #ff0000 (\lnot\sub\e) " with precedence 19 
 for @{ 'Not_elim_ko_2 $ab $a $b }.
 interpretation "Not_elim_ko_2" 'Not_elim_ko_2 ab a b = 
-  (cast _ _ (show b (cast _ _ (Not_elim _ (cast _ _ ab) a)))).
+  (cast _ _ (show b (cast _ _ (Not_elim _ (cast _ _ ab) (cast _ _ a))))).
 
 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (\lnot\sub\e) " with precedence 19 
 for @{ 'Not_elim_ok_1 $ab $a $b }.
@@ -449,8 +449,10 @@ interpretation "Not_elim_ok_2" 'Not_elim_ok_2 ab a b =
 
 notation > "¬_'e' term 90 ab term 90 a" with precedence 19
 for @{ 'Not_elim (show $ab ?) (show $a ?) }.
-interpretation "Not_elim KO" 'Not_elim ab a = (cast _ unit (Not_elim _ (cast _ _ ab) a)).
-interpretation "Not_elim OK" 'Not_elim ab a = (Not_elim _ ab a).
+interpretation "Not_elim KO" 'Not_elim ab a = 
+  (cast _ _ (Not_elim unit (cast _ _ ab) (cast _ _ a))).
+interpretation "Not_elim OK" 'Not_elim ab a = 
+  (Not_elim _ ab a).
 
 (* RAA *)
 notation < "\infrule hbox(\emsp Px \emsp) Pn (mstyle color #ff0000 (\RAA) \emsp ident x)" with precedence 19