src/HOL/Datatype.thy
changeset 29580 117b88da143c
parent 29183 f1648e009dc1
child 29609 a010aab5bed0
equal deleted inserted replaced
29579:cb520b766e00 29580:117b88da143c
     1 (*  Title:      HOL/Datatype.thy
     1 (*  Title:      HOL/Datatype.thy
     2     ID:         $Id$
       
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
     3     Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
     5 
     4 
     6 Could <*> be generalized to a general summation (Sigma)?
     5 Could <*> be generalized to a general summation (Sigma)?
     7 *)
     6 *)