From 0ed4641b6d1425d08602da42d4f4df614b4641e4 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 23 Mar 2010 15:59:10 +0000
Subject: [PATCH] symmetric_eq -> sym_eq

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>
---
 helm/software/matita/nlibrary/basics/list.ma | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/helm/software/matita/nlibrary/basics/list.ma b/helm/software/matita/nlibrary/basics/list.ma
index 3d41b946c..94ef847b0 100644
--- a/helm/software/matita/nlibrary/basics/list.ma
+++ b/helm/software/matita/nlibrary/basics/list.ma
@@ -80,7 +80,7 @@ ntheorem cons_append_commute:
 //; nqed. *)
 
 ntheorem append_cons:∀A.∀a:A.∀l,l1.l@(a::l1)=(l@[a])@l1.
-#A; #a; #l; #l1; napply symmetric_eq.
+#A; #a; #l; #l1; napply sym_eq.
 napply associative_append.
 (* /2/; *) nqed.
 
-- 
2.39.2