X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Ftutorial%2Fchapter12.ma;h=72e396c133ea84026a0898fae69eb4069d488eef;hb=053be41a8db6aa0ca7cc06fb569ec284a9bcc5ef;hp=a4f47c1ffa7c38cca91315c5747385c9fb5a8628;hpb=836e4f30514bceb27394604bbfbae31a62723dae;p=helm.git

diff --git a/matita/matita/lib/tutorial/chapter12.ma b/matita/matita/lib/tutorial/chapter12.ma
index a4f47c1ff..72e396c13 100644
--- a/matita/matita/lib/tutorial/chapter12.ma
+++ b/matita/matita/lib/tutorial/chapter12.ma
@@ -50,7 +50,7 @@ record setoid : Type[1] ≝ {
 (* Note that carrier has been defined as a coercion so that when S is a setoid
  we can write x:S in place of x: carrier S. *)
 
-(* We use the notation ≃ for the equality over setoid elements. *)
+(* We use the notation ≃ for the equality on setoid elements. *)
 notation "hvbox(n break ≃ m)"
   non associative with precedence 45
 for @{ 'congruent $n $m }.