1.1 --- a/src/HOL/List.thy	Thu Jun 05 13:19:27 1997 +0200
     1.2 +++ b/src/HOL/List.thy	Thu Jun 05 13:20:18 1997 +0200
     1.3 @@ -11,7 +11,6 @@
     1.4  datatype 'a list = "[]" ("[]") | "#" 'a ('a list) (infixr 65)
     1.5  
     1.6  consts
     1.7 -  pred_list  :: "('a list * 'a list) set"
     1.8    "@"         :: ['a list, 'a list] => 'a list            (infixr 65)
     1.9    filter      :: ['a => bool, 'a list] => 'a list
    1.10    concat      :: 'a list list => 'a list
    1.11 @@ -54,9 +53,6 @@
    1.12      Cons "[| a: A;  l: lists A |] ==> a#l : lists A"
    1.13  
    1.14  
    1.15 -rules
    1.16 -  pred_list_def "pred_list == {(x,y). ? h. y = h#x}"
    1.17 -
    1.18  primrec hd list
    1.19    "hd([]) = arbitrary"
    1.20    "hd(x#xs) = x"