# HG changeset patch
# User paulson
# Date 864643109 -7200
# Node ID ec3b55fcb165628c42285ec0908f365af6b21fb8
# Parent  89fe22bf9f546f646a9ac9dafd7cf0ca4af26668
New operator "lists" for formalizing sets of lists

diff -r 89fe22bf9f54 -r ec3b55fcb165 src/HOL/List.ML
--- a/src/HOL/List.ML	Mon May 26 12:37:24 1997 +0200
+++ b/src/HOL/List.ML	Mon May 26 12:38:29 1997 +0200
@@ -19,12 +19,12 @@
 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 operator over sets **)
+
+goalw thy lists.defs "!!A B. A<=B ==> lists A <= lists B";
+by (rtac lfp_mono 1);
+by (REPEAT (ares_tac basic_monos 1));
+qed "lists_mono";
 
 
 (** list_case **)
diff -r 89fe22bf9f54 -r ec3b55fcb165 src/HOL/List.thy
--- a/src/HOL/List.thy	Mon May 26 12:37:24 1997 +0200
+++ b/src/HOL/List.thy	Mon May 26 12:38:29 1997 +0200
@@ -45,6 +45,15 @@
   "@filter"   :: [idt, 'a list, bool] => 'a list          ("(1[_\\<in>_ ./ _])")
 
 
+consts
+  lists        :: 'a set => 'a list set
+
+  inductive "lists A"
+  intrs
+    Nil  "[]: lists A"
+    Cons "[| a: A;  l: lists A |] ==> a#l : lists A"
+
+
 rules
   pred_list_def "pred_list == {(x,y). ? h. y = h#x}"