src/HOL/Quotient.thy
changeset 51112 da97167e03f7
parent 48891 c0eafbd55de3
child 53011 aeee0a4be6cf
--- a/src/HOL/Quotient.thy	Thu Feb 14 13:16:47 2013 +0100
+++ b/src/HOL/Quotient.thy	Thu Feb 14 12:24:42 2013 +0100
@@ -5,7 +5,7 @@
 header {* Definition of Quotient Types *}
 
 theory Quotient
-imports Plain Hilbert_Choice Equiv_Relations Lifting
+imports Hilbert_Choice Equiv_Relations Lifting
 keywords
   "print_quotmapsQ3" "print_quotientsQ3" "print_quotconsts" :: diag and
   "quotient_type" :: thy_goal and "/" and