changeset 29580 | 117b88da143c |
parent 29183 | f1648e009dc1 |
child 29609 | a010aab5bed0 |
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 *) |