equal
deleted
inserted
replaced
1 (*<*) |
1 (* $Id$ *) |
|
2 |
2 theory Examples3 |
3 theory Examples3 |
3 imports Examples |
4 imports Examples |
4 begin |
5 begin |
5 |
|
6 (*>*) |
|
7 |
6 |
8 subsection {* Third Version: Local Interpretation *} |
7 subsection {* Third Version: Local Interpretation *} |
9 |
8 |
10 text {* In the above example, the fact that @{text \<le>} is a partial |
9 text {* In the above example, the fact that @{text \<le>} is a partial |
11 order for the natural numbers was used in the proof of the |
10 order for the natural numbers was used in the proof of the |
538 |
537 |
539 text {* \textbf{Acknowledgements.} Alexander Krauss, Tobias Nipkow, |
538 text {* \textbf{Acknowledgements.} Alexander Krauss, Tobias Nipkow, |
540 Christian Sternagel and Makarius Wenzel have made useful comments on |
539 Christian Sternagel and Makarius Wenzel have made useful comments on |
541 a draft of this document. *} |
540 a draft of this document. *} |
542 |
541 |
543 (*<*) |
|
544 end |
542 end |
545 (*>*) |
|