From: matitaweb Date: Tue, 28 Feb 2012 08:23:15 +0000 (+0000) Subject: commit by user utente2 X-Git-Tag: make_still_working~1934 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=69e4002db716a61af40c079d578eae0028c4316c;p=helm.git commit by user utente2 --- diff --git a/weblib/basics/core_notation.ma b/weblib/basics/core_notation.ma index 098b5d419..12c1a6d7e 100644 --- a/weblib/basics/core_notation.ma +++ b/weblib/basics/core_notation.ma @@ -74,6 +74,8 @@ for @{ 'congruent $n $m $p }. notation "hvbox(\langle term 19 a, break term 19 b\rangle)" with precedence 90 for @{ 'pair $a $b}. +notation "hvbox(〈term 19 a, break term 19 b〉)" +with precedence 90 for @{ 'pair $a $b}. notation "hvbox(x break \times y)" with precedence 70 for @{ 'product $x $y}. diff --git a/weblib/basics/types.ma b/weblib/basics/types.ma index 586ce31ce..a07cf29ea 100644 --- a/weblib/basics/types.ma +++ b/weblib/basics/types.ma @@ -39,7 +39,7 @@ interpretation "pair pi1" 'pi1b x y = (fst ? ? x y). interpretation "pair pi2" 'pi2b x y = (snd ? ? x y). theorem eq_pair_fst_snd: ∀A,B.∀p:A a title="Product" href="cic:/fakeuri.def(1)"×/a B. - p a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a p, a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a p 〉. + p a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a p, a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a p 〉. #A #B #p (cases p) // qed. (* sum *)