# HG changeset patch
# User kuncar
# Date 1332523427 -3600
# Node ID e64ffc96a49f07089544f478960f1fc02637e218
# Parent  b846c299f412dce687e17f73f59ca5041c2beb3c
hide invariant constant

diff -r b846c299f412 -r e64ffc96a49f src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Fri Mar 23 16:16:35 2012 +0000
+++ b/src/HOL/Quotient.thy	Fri Mar 23 18:23:47 2012 +0100
@@ -960,4 +960,6 @@
   map_fun (infixr "--->" 55) and
   fun_rel (infixr "===>" 55)
 
+hide_const (open) invariant
+
 end