equal
deleted
inserted
replaced
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 *) |
4 *) |
5 |
5 |
6 header {* The Axiom of Choice Holds in L! *} |
6 header {* The Axiom of Choice Holds in L! *} |
7 |
7 |
8 theory AC_in_L = Formula: |
8 theory AC_in_L imports Formula begin |
9 |
9 |
10 subsection{*Extending a Wellordering over a List -- Lexicographic Power*} |
10 subsection{*Extending a Wellordering over a List -- Lexicographic Power*} |
11 |
11 |
12 text{*This could be moved into a library.*} |
12 text{*This could be moved into a library.*} |
13 |
13 |