changeset 41413 | 64cd30d6b0b8 |
parent 40928 | ace26e2cee91 |
child 41467 | 8fc17c5e11c0 |
--- a/src/HOL/Quotient_Examples/Quotient_Int.thy Wed Dec 29 13:51:17 2010 +0100 +++ b/src/HOL/Quotient_Examples/Quotient_Int.thy Wed Dec 29 17:34:41 2010 +0100 @@ -5,7 +5,7 @@ Integers based on Quotients, based on an older version by Larry Paulson. *) theory Quotient_Int -imports Quotient_Product Nat +imports "~~/src/HOL/Library/Quotient_Product" Nat begin fun