From dbce2f96c977d51ac2843e98a224aa4dae7ea3b2 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 15 Nov 2008 15:20:33 +0000 Subject: [PATCH] fixed not-e --- .../matita/library/didactic/support/natural_deduction.ma | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/matita/library/didactic/support/natural_deduction.ma b/helm/software/matita/library/didactic/support/natural_deduction.ma index 3e7c54d5c..b7ee07cb6 100644 --- a/helm/software/matita/library/didactic/support/natural_deduction.ma +++ b/helm/software/matita/library/didactic/support/natural_deduction.ma @@ -450,7 +450,7 @@ 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 _ _ (Not_elim _ (cast _ _ ab) (cast _ _ a))). + (cast _ _ (Not_elim unit (cast _ _ ab) (cast _ _ a))). interpretation "Not_elim OK" 'Not_elim ab a = (Not_elim _ ab a). -- 2.39.2