--- a/src/HOL/List.thy Thu Jun 05 13:19:27 1997 +0200
+++ b/src/HOL/List.thy Thu Jun 05 13:20:18 1997 +0200
@@ -11,7 +11,6 @@
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
@@ -54,9 +53,6 @@
Cons "[| a: A; l: lists A |] ==> a#l : lists A"
-rules
- pred_list_def "pred_list == {(x,y). ? h. y = h#x}"
-
primrec hd list
"hd([]) = arbitrary"
"hd(x#xs) = x"