src/HOL/Quotient.thy
changeset 46950 d0181abdbdac
parent 46947 b8c7eb0c2f89
child 47091 d5cd13aca90b
     1.1 --- a/src/HOL/Quotient.thy	Thu Mar 15 20:07:00 2012 +0100
     1.2 +++ b/src/HOL/Quotient.thy	Thu Mar 15 22:08:53 2012 +0100
     1.3 @@ -6,7 +6,10 @@
     1.4  
     1.5  theory Quotient
     1.6  imports Plain Hilbert_Choice Equiv_Relations
     1.7 -keywords "/"
     1.8 +keywords
     1.9 +  "print_quotmaps" "print_quotients" "print_quotconsts" :: diag and
    1.10 +  "quotient_type" :: thy_goal and "/" and
    1.11 +  "quotient_definition" :: thy_decl
    1.12  uses
    1.13    ("Tools/Quotient/quotient_info.ML")
    1.14    ("Tools/Quotient/quotient_type.ML")