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

src/HOL/Library/Quotient_Set.thy

changeset 60500 | 903bb1495239 |

parent 58881 | b9556a055632 |

child 62954 | c5d0fdc260fa |

1.1 --- a/src/HOL/Library/Quotient_Set.thy Wed Jun 17 10:57:11 2015 +0200 1.2 +++ b/src/HOL/Library/Quotient_Set.thy Wed Jun 17 11:03:05 2015 +0200 1.3 @@ -2,13 +2,13 @@ 1.4 Author: Cezary Kaliszyk and Christian Urban 1.5 *) 1.6 1.7 -section {* Quotient infrastructure for the set type *} 1.8 +section \<open>Quotient infrastructure for the set type\<close> 1.9 1.10 theory Quotient_Set 1.11 imports Main Quotient_Syntax 1.12 begin 1.13 1.14 -subsection {* Contravariant set map (vimage) and set relator, rules for the Quotient package *} 1.15 +subsection \<open>Contravariant set map (vimage) and set relator, rules for the Quotient package\<close> 1.16 1.17 definition "rel_vset R xs ys \<equiv> \<forall>x y. R x y \<longrightarrow> x \<in> xs \<longleftrightarrow> y \<in> ys" 1.18