doc-src/Intro/list.thy
author slotosch
Wed, 26 Mar 1997 13:44:05 +0100
changeset 2840 7e03e61612b0
parent 105 216d6ed87399
child 32960 69916a850301
permissions -rw-r--r--
generalized theorems and class instances for Cprod. Now "*"::(cpo,cpo)cpo and "*"::(pcpo,pcpo)pcpo

List = FOL +
types 	list 1
arities list	:: (term)term
consts	Nil	:: "'a list"
   	Cons	:: "['a, 'a list] => 'a list" 
end