changeset 51112 | da97167e03f7 |
parent 49962 | a8cc904a6820 |
child 51143 | 0a2371e7ced3 |
--- a/src/HOL/Int.thy Thu Feb 14 13:16:47 2013 +0100 +++ b/src/HOL/Int.thy Thu Feb 14 12:24:42 2013 +0100 @@ -6,7 +6,7 @@ header {* The Integers as Equivalence Classes over Pairs of Natural Numbers *} theory Int -imports Equiv_Relations Wellfounded Quotient +imports Equiv_Relations Wellfounded Quotient FunDef begin subsection {* Definition of integers as a quotient type *}