# HG changeset patch
# User paulson
# Date 865509618 -7200
# Node ID 862e153afc128bb244f7ede755f6f63757efeb71
# Parent  80c979e0d42f02c87c3576c380b8b6c075ba017e
Deleted the obsolete "pred_list" relation

diff -r 80c979e0d42f -r 862e153afc12 src/HOL/List.thy
--- 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"