hide invariant constant
authorkuncar
Fri Mar 23 18:23:47 2012 +0100 (2012-03-23)
changeset 47105e64ffc96a49f
parent 47102 b846c299f412
child 47106 dfa5ed8d94b4
hide invariant constant
src/HOL/Quotient.thy
     1.1 --- a/src/HOL/Quotient.thy	Fri Mar 23 16:16:35 2012 +0000
     1.2 +++ b/src/HOL/Quotient.thy	Fri Mar 23 18:23:47 2012 +0100
     1.3 @@ -960,4 +960,6 @@
     1.4    map_fun (infixr "--->" 55) and
     1.5    fun_rel (infixr "===>" 55)
     1.6  
     1.7 +hide_const (open) invariant
     1.8 +
     1.9  end