src/HOL/Quotient.thy
changeset 47105 e64ffc96a49f
parent 47096 3ea48c19673e
child 47308 9caab698dbe4
child 47434 b75ce48a93ee
equal deleted inserted replaced
47102:b846c299f412 47105:e64ffc96a49f
   958 no_notation
   958 no_notation
   959   rel_conj (infixr "OOO" 75) and
   959   rel_conj (infixr "OOO" 75) and
   960   map_fun (infixr "--->" 55) and
   960   map_fun (infixr "--->" 55) and
   961   fun_rel (infixr "===>" 55)
   961   fun_rel (infixr "===>" 55)
   962 
   962 
       
   963 hide_const (open) invariant
       
   964 
   963 end
   965 end