src/HOL/Quotient.thy
changeset 57960 ee1ba4848896
parent 56073 29e308b56d23
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Quotient.thy	Sat Aug 16 19:20:11 2014 +0200
     1.2 +++ b/src/HOL/Quotient.thy	Sat Aug 16 20:14:45 2014 +0200
     1.3 @@ -748,8 +748,12 @@
     1.4  
     1.5  text {* Auxiliary data for the quotient package *}
     1.6  
     1.7 +named_theorems quot_equiv "equivalence relation theorems"
     1.8 +named_theorems quot_respect "respectfulness theorems"
     1.9 +named_theorems quot_preserve "preservation theorems"
    1.10 +named_theorems id_simps "identity simp rules for maps"
    1.11 +named_theorems quot_thm "quotient theorems"
    1.12  ML_file "Tools/Quotient/quotient_info.ML"
    1.13 -setup Quotient_Info.setup
    1.14  
    1.15  declare [[mapQ3 "fun" = (rel_fun, fun_quotient3)]]
    1.16