src/HOL/Quotient.thy
changeset 59028 df7476e79558
parent 58889 5b7a9633cfa8
child 60758 d8d85a8172b5
     1.1 --- a/src/HOL/Quotient.thy	Fri Nov 21 22:59:32 2014 +0100
     1.2 +++ b/src/HOL/Quotient.thy	Sat Nov 22 11:36:00 2014 +0100
     1.3 @@ -749,10 +749,10 @@
     1.4  text {* Auxiliary data for the quotient package *}
     1.5  
     1.6  named_theorems quot_equiv "equivalence relation theorems"
     1.7 -named_theorems quot_respect "respectfulness theorems"
     1.8 -named_theorems quot_preserve "preservation theorems"
     1.9 -named_theorems id_simps "identity simp rules for maps"
    1.10 -named_theorems quot_thm "quotient theorems"
    1.11 +  and quot_respect "respectfulness theorems"
    1.12 +  and quot_preserve "preservation theorems"
    1.13 +  and id_simps "identity simp rules for maps"
    1.14 +  and quot_thm "quotient theorems"
    1.15  ML_file "Tools/Quotient/quotient_info.ML"
    1.16  
    1.17  declare [[mapQ3 "fun" = (rel_fun, fun_quotient3)]]