--- 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 **)
--- 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}"