--- a/src/HOL/List.thy Thu May 15 12:53:39 1997 +0200
+++ b/src/HOL/List.thy Thu May 15 12:54:02 1997 +0200
@@ -11,7 +11,7 @@
datatype 'a list = "[]" ("[]") | "#" 'a ('a list) (infixr 65)
consts
-
+ pred_list :: "('a list * 'a list) set"
"@" :: ['a list, 'a list] => 'a list (infixr 65)
filter :: ['a => bool, 'a list] => 'a list
concat :: 'a list list => 'a list
@@ -45,6 +45,9 @@
"@filter" :: [idt, 'a list, bool] => 'a list ("(1[_\\<in>_ ./ _])")
+rules
+ pred_list_def "pred_list == {(x,y). ? h. y = h#x}"
+
primrec hd list
"hd([]) = (@x.False)"
"hd(x#xs) = x"
@@ -100,4 +103,5 @@
primrec dropWhile list
"dropWhile P [] = []"
"dropWhile P (x#xs) = (if P x then dropWhile P xs else xs)"
+
end