equal
deleted
inserted
replaced
3 *) |
3 *) |
4 |
4 |
5 header {* Extending Well-founded Relations to Wellorders *} |
5 header {* Extending Well-founded Relations to Wellorders *} |
6 |
6 |
7 theory Wellorder_Extension |
7 theory Wellorder_Extension |
8 imports "~~/src/HOL/Library/Zorn" Order_Union |
8 imports Zorn Order_Union |
9 begin |
9 begin |
10 |
10 |
11 subsection {* Extending Well-founded Relations to Wellorders *} |
11 subsection {* Extending Well-founded Relations to Wellorders *} |
12 |
12 |
13 text {*A \emph{downset} (also lower set, decreasing set, initial segment, or |
13 text {*A \emph{downset} (also lower set, decreasing set, initial segment, or |