src/HOL/List.thy
changeset 3342 ec3b55fcb165
parent 3320 3a5e4930fb77
child 3367 832c245d967c
--- 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}"