]> matita.cs.unibo.it Git - helm.git/commitdiff
Nil => nil; Cons => cons
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sun, 28 Oct 2007 16:07:10 +0000 (16:07 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sun, 28 Oct 2007 16:07:10 +0000 (16:07 +0000)
helm/software/matita/library/demo/propositional_sequent_calculus.ma

index d79cd2e6ddded90916b5a01f48d00d305dafd225..32e11054c5d19bdb699f77578b4fa60fd1c83154 100644 (file)
@@ -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 ≝