# HG changeset patch
# User paulson
# Date 863693642 -7200
# Node ID c522bc46aea78653aeb497c90ce427571130cb5a
# Parent  dcb458d38724801287b35b8ea5f1e1b4381a7f66
Added pred_list for TFL

diff -r dcb458d38724 -r c522bc46aea7 src/HOL/List.ML
--- a/src/HOL/List.ML	Thu May 15 12:53:39 1997 +0200
+++ b/src/HOL/List.ML	Thu May 15 12:54:02 1997 +0200
@@ -19,6 +19,14 @@
 qed "neq_Nil_conv";
 
 
+goalw thy [wf_def, pred_list_def] "wf(pred_list)";
+by (strip_tac 1);
+by (induct_tac "x" 1);
+by (ALLGOALS Blast_tac);
+qed "wf_pred_list";
+AddIffs [wf_pred_list];
+
+
 (** list_case **)
 
 goal thy
diff -r dcb458d38724 -r c522bc46aea7 src/HOL/List.thy
--- 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