| 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 *}