| changeset 16417 | 9bc16273c2d4 |
| parent 11456 | 7eb63f63e6c6 |
| child 27321 | 464ac1c815ec |
--- a/doc-src/TutorialI/Misc/pairs.thy Fri Jun 17 11:35:35 2005 +0200 +++ b/doc-src/TutorialI/Misc/pairs.thy Fri Jun 17 16:12:49 2005 +0200 @@ -1,5 +1,5 @@ (*<*) -theory pairs = Main:; +theory pairs imports Main begin; (*>*) text{*\label{sec:pairs}\index{pairs and tuples} HOL also has ordered pairs: \isa{($a@1$,$a@2$)} is of type $\tau@1$