]> matita.cs.unibo.it Git - helm.git/commitdiff
...
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 16 Mar 2010 14:17:51 +0000 (14:17 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 16 Mar 2010 14:17:51 +0000 (14:17 +0000)
helm/software/matita/nlibrary/Plogic/connectives.ma

index 84bd36454064e90ba35f74df324a28cb8407f83f..491657676a85ada0ae073947190306fedbb0af87 100644 (file)
@@ -30,8 +30,6 @@ ndefinition Not: Prop → Prop ≝
 ninductive Not (A:Prop): Prop ≝
 nmk: (A → False) → Not A.
 
-ncheck Not_ind.
-
 interpretation "logical not" 'not x = (Not x).
 
 ntheorem absurd : ∀ A:Prop. A → ¬A → False.