| changeset 55085 | 0e8e4dc55866 | 
| parent 54863 | 82acc20ded73 | 
| child 55096 | 916b2ac758f4 | 
--- a/src/HOL/Int.thy Mon Jan 20 20:42:43 2014 +0100 +++ b/src/HOL/Int.thy Mon Jan 20 21:32:41 2014 +0100 @@ -6,7 +6,7 @@ header {* The Integers as Equivalence Classes over Pairs of Natural Numbers *} theory Int -imports Equiv_Relations Wellfounded Quotient FunDef +imports Equiv_Relations Wellfounded Quotient Fun_Def begin subsection {* Definition of integers as a quotient type *}