From: Stefano Zacchiroli Date: Wed, 14 Jun 2006 14:33:57 +0000 (+0000) Subject: fixed bad spellend "stantard" X-Git-Tag: make_still_working~7189 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=abd976fb6603a85c1da6d1582114e7c1fa472449;p=helm.git fixed bad spellend "stantard" --- diff --git a/helm/software/matita/library/nat/permutation.ma b/helm/software/matita/library/nat/permutation.ma index 9ab0358c5..768e0bd60 100644 --- a/helm/software/matita/library/nat/permutation.ma +++ b/helm/software/matita/library/nat/permutation.ma @@ -73,7 +73,18 @@ match eqb n i with match eqb n j with [ true \Rightarrow i | false \Rightarrow n]]. - + +notation < "(❲i↹j❳)n" + right associative with precedence 71 +for @{ 'transposition $i $j $n}. + +notation < "(❲i \atop j❳)n" + right associative with precedence 71 +for @{ 'transposition $i $j $n}. + +interpretation "natural transposition" 'transposition i j n = + (cic:/matita/nat/permutation/transpose.con i j n). + lemma transpose_i_j_i: \forall i,j:nat. transpose i j i = j. intros.unfold transpose. rewrite > (eqb_n_n i).simplify. reflexivity. diff --git a/helm/software/matita/matita.conf.xml.in b/helm/software/matita/matita.conf.xml.in index b016367e9..90aafb73d 100644 --- a/helm/software/matita/matita.conf.xml.in +++ b/helm/software/matita/matita.conf.xml.in @@ -57,7 +57,7 @@ --> cic:/matita/ - file://@RT_BASE_DIR@/xml/stantard-library/ + file://@RT_BASE_DIR@/xml/standard-library/ ro