src/HOL/List.thy
changeset 6141 a6922171b396
parent 5518 654ead0ba4f7
child 6306 81e7fbf61db2
     1.1 --- a/src/HOL/List.thy	Tue Jan 19 11:16:39 1999 +0100
     1.2 +++ b/src/HOL/List.thy	Tue Jan 19 11:18:11 1999 +0100
     1.3 @@ -114,8 +114,8 @@
     1.4    "filter P [] = []"
     1.5    "filter P (x#xs) = (if P x then x#filter P xs else filter P xs)"
     1.6  primrec
     1.7 -  "foldl f a [] = a"
     1.8 -  "foldl f a (x#xs) = foldl f (f a x) xs"
     1.9 +  foldl_Nil  "foldl f a [] = a"
    1.10 +  foldl_Cons "foldl f a (x#xs) = foldl f (f a x) xs"
    1.11  primrec
    1.12    "concat([]) = []"
    1.13    "concat(x#xs) = x @ concat(xs)"