equal
deleted
inserted
replaced
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 *) |
3 *) |
4 |
4 |
5 section \<open>Closed Unbounded Classes and Normal Functions\<close> |
5 section \<open>Closed Unbounded Classes and Normal Functions\<close> |
6 |
6 |
7 theory Normal imports Main begin |
7 theory Normal imports ZF begin |
8 |
8 |
9 text\<open> |
9 text\<open> |
10 One source is the book |
10 One source is the book |
11 |
11 |
12 Frank R. Drake. |
12 Frank R. Drake. |