| changeset 58860 | fee7cfa69c50 |
| parent 48985 | 5386df44a037 |
| child 67406 | 23307fd33906 |
--- a/src/Doc/Tutorial/Misc/pairs2.thy Sat Nov 01 11:40:55 2014 +0100 +++ b/src/Doc/Tutorial/Misc/pairs2.thy Sat Nov 01 14:20:38 2014 +0100 @@ -1,5 +1,5 @@ (*<*) -theory pairs2 imports Main begin; +theory pairs2 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$