# HG changeset patch
# User paulson
# Date 941802435 -3600
# Node ID acafa0f151316a9818571cf1239180195eb7b16f
# Parent  7acf6eb8eec1d2a004ff84c8de5b92ca802ce74d
added foldr

diff -r 7acf6eb8eec1 -r acafa0f15131 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Nov 05 12:45:37 1999 +0100
+++ b/src/HOL/List.thy	Fri Nov 05 12:47:15 1999 +0100
@@ -15,6 +15,7 @@
   filter      :: ['a => bool, 'a list] => 'a list
   concat      :: 'a list list => 'a list
   foldl       :: [['b,'a] => 'b, 'b, 'a list] => 'b
+  foldr       :: [['a,'b] => 'b, 'a list, 'b] => 'b
   hd, last    :: 'a list => 'a
   set         :: 'a list => 'a set
   list_all    :: ('a => bool) => ('a list => bool)
@@ -117,6 +118,9 @@
   foldl_Nil  "foldl f a [] = a"
   foldl_Cons "foldl f a (x#xs) = foldl f (f a x) xs"
 primrec
+  "foldr f [] a = a"
+  "foldr f (x#xs) a = f x (foldr f xs a)"
+primrec
   "concat([]) = []"
   "concat(x#xs) = x @ concat(xs)"
 primrec