changeset 30738 | 0842e906300c |
parent 29608 | 564ea783ace8 |
--- a/src/HOL/Library/Quotient.thy Fri Mar 27 10:05:08 2009 +0100 +++ b/src/HOL/Library/Quotient.thy Fri Mar 27 10:05:11 2009 +0100 @@ -1,12 +1,11 @@ (* Title: HOL/Library/Quotient.thy - ID: $Id$ Author: Markus Wenzel, TU Muenchen *) header {* Quotient types *} theory Quotient -imports Plain "~~/src/HOL/Hilbert_Choice" +imports Main begin text {*