]> matita.cs.unibo.it Git - helm.git/commitdiff
neg => Qneg :-)
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 25 Oct 2007 17:10:25 +0000 (17:10 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 25 Oct 2007 17:10:25 +0000 (17:10 +0000)
helm/software/matita/library/Q/q.ma

index 23ef525519b42282aa10185e14604e3a12fa8fcc..072532d7bc7a4c8732486f5886a9147f082d5523 100644 (file)
@@ -330,7 +330,7 @@ definition Qtimes : Q \to Q \to Q \def
     |Qpos q1 \Rightarrow Qpos (rtimes p1 q1)
     |Qneg q1 \Rightarrow Qneg (rtimes p1 q1)
     ]
-  |neg p1 \Rightarrow 
+  |Qneg p1 \Rightarrow 
     match q with
     [OQ \Rightarrow OQ
     |Qpos q1 \Rightarrow Qneg (rtimes p1 q1)