| changeset 58770 | ae5e9b4f8daf |
| parent 58710 | 7216a10d69ba |
| child 58834 | 773b378d9313 |
--- a/src/HOL/Library/Nat_Bijection.thy Thu Oct 23 14:04:05 2014 +0200 +++ b/src/HOL/Library/Nat_Bijection.thy Thu Oct 23 14:04:05 2014 +0200 @@ -9,7 +9,7 @@ header {* Bijections between natural numbers and other types *} theory Nat_Bijection -imports Main Parity +imports Main begin subsection {* Type @{typ "nat \<times> nat"} *}