| changeset 16417 | 9bc16273c2d4 |
| parent 14171 | 0cab06e3bbd0 |
| child 21233 | 5a5c8ea5f66a |
| 16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
|---|---|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 *) |
4 *) |
5 |
5 |
6 header {*Closed Unbounded Classes and Normal Functions*} |
6 header {*Closed Unbounded Classes and Normal Functions*} |
7 |
7 |
8 theory Normal = Main: |
8 theory Normal imports Main begin |
9 |
9 |
10 text{* |
10 text{* |
11 One source is the book |
11 One source is the book |
12 |
12 |
13 Frank R. Drake. |
13 Frank R. Drake. |