X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Fordered_group.ma;fp=helm%2Fsoftware%2Fmatita%2Fdama%2Fordered_group.ma;h=d2f96fb5c7c03faf6fdb1b76774fd49dd8c86c14;hb=39c55604f8114e2e8f9f9769acd328de8f19c7e4;hp=5b0f0aa9b6c0c386b1c06ed3cb9184d1a6aeb320;hpb=0e93f77172427eed198b974e32c7f3e80d2c0251;p=helm.git

diff --git a/helm/software/matita/dama/ordered_group.ma b/helm/software/matita/dama/ordered_group.ma
index 5b0f0aa9b..d2f96fb5c 100644
--- a/helm/software/matita/dama/ordered_group.ma
+++ b/helm/software/matita/dama/ordered_group.ma
@@ -37,18 +37,6 @@ record ogroup : Type ≝ {
   exc_canc_plusr: ∀f,g,h:og_carr. f+h ≰ g+h → f ≰ g
 }.
 
-notation > "'Ex'≪" non associative with precedence 50 for
- @{'excedencerewritel}.
- 
-interpretation "exc_rewl" 'excedencerewritel = 
- (cic:/matita/excedence/exc_rewl.con _ _ _).
-
-notation > "'Ex'≫" non associative with precedence 50 for
- @{'excedencerewriter}.
- 
-interpretation "exc_rewr" 'excedencerewriter = 
- (cic:/matita/excedence/exc_rewr.con _ _ _).
-
 lemma fexc_plusr: 
   ∀G:ogroup.∀x,y,z:G. x ≰ y → x+z ≰ y + z.
 intros 5 (G x y z L); apply (exc_canc_plusr ??? (-z));
@@ -196,6 +184,5 @@ apply (le_rewr ??? b (zero_neutral ??));
 assumption;
 qed.
 
-
   
   
\ No newline at end of file