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