From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 28 Oct 2007 16:07:10 +0000 (+0000)
Subject: Nil => nil; Cons => cons
X-Git-Tag: 0.4.95@7852~82
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=aadde7ee6f137e88952113dc8d3d173f5c7bfc30

Nil => nil; Cons => cons
---

diff --git a/matita/library/demo/propositional_sequent_calculus.ma b/matita/library/demo/propositional_sequent_calculus.ma
index d79cd2e6d..32e11054c 100644
--- a/matita/library/demo/propositional_sequent_calculus.ma
+++ b/matita/library/demo/propositional_sequent_calculus.ma
@@ -163,11 +163,10 @@ let rec and_of_list l ≝
   | cons F l' ⇒ FAnd F (and_of_list l')
   ].
 
-alias id "Nil" = "cic:/matita/list/list.ind#xpointer(1/1/1)".
 let rec or_of_list l ≝
  match l with
-  [ Nil ⇒ FFalse
-  | Cons F l' ⇒ FOr F (or_of_list l')
+  [ nil ⇒ FFalse
+  | cons F l' ⇒ FOr F (or_of_list l')
   ].
 
 definition formula_of_sequent ≝