summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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)]]