| changeset 55096 | 916b2ac758f4 |
| parent 55085 | 0e8e4dc55866 |
| child 55404 | 5cb95b79a51f |
--- a/src/HOL/Int.thy Tue Jan 21 13:05:22 2014 +0100 +++ b/src/HOL/Int.thy Tue Jan 21 13:21:55 2014 +0100 @@ -6,7 +6,7 @@ header {* The Integers as Equivalence Classes over Pairs of Natural Numbers *} theory Int -imports Equiv_Relations Wellfounded Quotient Fun_Def +imports Equiv_Relations Wellfounded Power Quotient Fun_Def begin subsection {* Definition of integers as a quotient type *}