commit by user utente2

diff --git a/weblib/basics/core_notation.ma b/weblib/basics/core_notation.ma
index 098b5d419d4f1620db3ca6e21ff3f96e3a996c80..12c1a6d7e224ebff92142356b998d81b8e36e8ce 100644 (file)
--- 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 586ce31ce7bb527d251d3d1a9ddf5704f9163a2a..a07cf29ea0e9c23f862e5ce04b311a2db7a99b3b 100644 (file)
--- 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 \ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6 B.
-  p \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6 \ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 p, \ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 p 〉.
+  p \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6 \ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 p, \ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 p 〉.
 #A #B #p (cases p) // qed.
 
 (* sum *)