src/Doc/Tutorial/Misc/pairs2.thy
changeset 58860 fee7cfa69c50
parent 48985 5386df44a037
child 67406 23307fd33906
     1.1 --- a/src/Doc/Tutorial/Misc/pairs2.thy	Sat Nov 01 11:40:55 2014 +0100
     1.2 +++ b/src/Doc/Tutorial/Misc/pairs2.thy	Sat Nov 01 14:20:38 2014 +0100
     1.3 @@ -1,5 +1,5 @@
     1.4  (*<*)
     1.5 -theory pairs2 imports Main begin;
     1.6 +theory pairs2 imports Main begin
     1.7  (*>*)
     1.8  text{*\label{sec:pairs}\index{pairs and tuples}
     1.9  HOL also has ordered pairs: \isa{($a@1$,$a@2$)} is of type $\tau@1$