| 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