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