From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 7 Jan 2015 16:48:33 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~769
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a57efb7e02d1c0af621ab36bd345f2f79f063a0c;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 }.
diff --git a/matita/matita/lib/tutorial/chapter8.ma b/matita/matita/lib/tutorial/chapter8.ma
index b9bc64a9c..427b14842 100644
--- a/matita/matita/lib/tutorial/chapter8.ma
+++ b/matita/matita/lib/tutorial/chapter8.ma
@@ -270,8 +270,8 @@ lemma sem_star_w : ∀S.∀i:pitem S.∀w.
 (* Below are a few, simple, semantic properties of items. In particular:
 - not_epsilon_item : ∀S:DeqSet.∀i:pitem S. ¬ (\sem{i} ϵ).
 - epsilon_pre : ∀S.∀e:pre S. (\sem{i} ϵ) ↔ (\snd e = true).
-- minus_eps_item: ∀S.∀i:pitem S. \sem{i} =1 \sem{i}-{[ ]}.
-- minus_eps_pre: ∀S.∀e:pre S. \sem{\fst e} =1 \sem{e}-{[ ]}.
+- minus_eps_item: ∀S.∀i:pitem S. \sem{i} ≐ \sem{i}-{[ ]}.
+- minus_eps_pre: ∀S.∀e:pre S. \sem{\fst e} ≐ \sem{e}-{[ ]}.
 The first property is proved by a simple induction on $i$; the other
 results are easy corollaries. We need an auxiliary lemma first. *)