From: Enrico Tassi Date: Fri, 19 Dec 2008 20:20:15 +0000 (+0000) Subject: fix exponentiation X-Git-Tag: make_still_working~4350 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=970430a378f27d4e5cc2a45dc2fa3d79bc9bf088;p=helm.git fix exponentiation --- diff --git a/helm/software/matita/core_notation.moo b/helm/software/matita/core_notation.moo index 98658726a..9970c9cfb 100644 --- a/helm/software/matita/core_notation.moo +++ b/helm/software/matita/core_notation.moo @@ -201,7 +201,8 @@ notation "hvbox(a break \circ b)" left associative with precedence 55 for @{ 'compose $a $b }. -notation "↓a" with precedence 55 for @{ 'downarrow $a }. +notation < "↓ \ensp a" with precedence 55 for @{ 'downarrow $a }. +notation > "↓ a" with precedence 55 for @{ 'downarrow $a }. notation "hvbox(U break ↓ V)" non associative with precedence 55 for @{ 'fintersects $U $V }. @@ -209,7 +210,8 @@ notation "↑a" with precedence 55 for @{ 'uparrow $a }. notation "hvbox(a break ↑ b)" with precedence 55 for @{ 'funion $a $b }. -notation "a \sup b" left associative with precedence 90 for @{ 'exp $a $b}. +notation "a \sup term 89 b" with precedence 90 for @{ 'exp $a $b}. +notation > "a ^ term 89 b" with precedence 90 for @{ 'exp $a $b}. notation "s \sup (-1)" with precedence 90 for @{ 'invert $s }. notation > "s ^ (-1)" with precedence 90 for @{ 'invert $s }. notation < "s \sup (-1) x" with precedence 90 for @{ 'invert_appl $s $x}. diff --git a/helm/software/matita/library/nat/factorization.ma b/helm/software/matita/library/nat/factorization.ma index 6226f3b6d..92f64e56d 100644 --- a/helm/software/matita/library/nat/factorization.ma +++ b/helm/software/matita/library/nat/factorization.ma @@ -526,7 +526,7 @@ split [apply lt_O_nth_prime_n |apply (lt_O_n_elim ? H). intro. - apply (witness ? ? (r*(nth_prime p \sup m))). + apply (witness ? ? ((r*(nth_prime p) \sup m))). rewrite < assoc_times. rewrite < sym_times in \vdash (? ? ? (? % ?)). rewrite > exp_n_SO in \vdash (? ? ? (? (? ? %) ?)).