From 1f946a70bc439ced80c695f0fd0c210df0d3b767 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 16 May 2012 20:33:41 +0000
Subject: [PATCH] Removed duplicated notation and interaction with the user.

---
 matita/matita/lib/basics/finset.ma      | 2 ++
 matita/matita/lib/basics/lists/listb.ma | 3 +--
 matita/matita/lib/re/moves.ma           | 4 +---
 3 files changed, 4 insertions(+), 5 deletions(-)

diff --git a/matita/matita/lib/basics/finset.ma b/matita/matita/lib/basics/finset.ma
index a8ee13a07..85f4ef3ba 100644
--- a/matita/matita/lib/basics/finset.ma
+++ b/matita/matita/lib/basics/finset.ma
@@ -102,6 +102,8 @@ definition FinSum ≝ λA,B:FinSet.
    (enum_sum A B (enum A) (enum B)) 
    (enumAB_unique … (enum_unique A) (enum_unique B)).
 
+include alias "basics/types.ma".
+
 unification hint  0 ≔ C1,C2; 
     T1 ≟ FinSetcarr C1,
     T2 ≟ FinSetcarr C2,
diff --git a/matita/matita/lib/basics/lists/listb.ma b/matita/matita/lib/basics/lists/listb.ma
index e46f45f07..7951f2997 100644
--- a/matita/matita/lib/basics/lists/listb.ma
+++ b/matita/matita/lib/basics/lists/listb.ma
@@ -31,8 +31,7 @@ let rec memb (S:DeqSet) (x:S) (l: list S) on l  ≝
   | cons a tl ⇒ (x == a) ∨ memb S x tl
   ].
 
-notation < "\memb x l" non associative with precedence 90 for @{'memb $x $l}.
-interpretation "boolean membership" 'memb a l = (memb ? a l).
+interpretation "boolean membership" 'mem a l = (memb ? a l).
 
 lemma memb_hd: ∀S,a,l. memb S a (a::l) = true.
 #S #a #l normalize >(proj2 … (eqb_true S …) (refl S a)) //
diff --git a/matita/matita/lib/re/moves.ma b/matita/matita/lib/re/moves.ma
index 6f6d0a67b..c8c3b3478 100644
--- a/matita/matita/lib/re/moves.ma
+++ b/matita/matita/lib/re/moves.ma
@@ -92,8 +92,7 @@ theorem move_ok:
    (* rhs = a::w1∈\sem{i1}\sem{|i2|} ∨ a::w∈\sem{i2} *)
    @iff_trans[||@(iff_or_l … (HI2 w))] 
    (* rhs = a::w1∈\sem{i1}\sem{|i2|} ∨ w∈\sem{move S a i2} *)
-   @iff_or_r 
-   check deriv_middot 
+   @iff_or_r
    (* we are left to prove that 
      w∈\sem{move S a i1}·\sem{|i2|} ↔ a::w∈\sem{i1}\sem{|i2|}
      we use deriv_middot on the rhs *)
@@ -145,7 +144,6 @@ theorem decidable_sem: ∀S:DeqSet.∀w: word S. ∀e:pre S.
 #S #w elim w 
  [* #i #b >moves_empty cases b % /2/
  |#a #w1 #Hind #e >moves_cons
- check not_epsilon_sem
   @iff_trans [||@iff_sym @not_epsilon_sem]
   @iff_trans [||@move_ok] @Hind
  ]
-- 
2.39.2