# HG changeset patch
# User blanchet
# Date 1392360826 -3600
# Node ID c582a7893dcddbfc63b8838b65900097a8f672c6
# Parent  990651bfc65b59433867ef8d4c18bb5ff2979c33
hide 'rel' name -- this one is waiting to be merged with 'list_all2'

diff -r 990651bfc65b -r c582a7893dcd src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Feb 14 07:53:46 2014 +0100
+++ b/src/HOL/List.thy	Fri Feb 14 07:53:46 2014 +0100
@@ -34,6 +34,8 @@
 
 setup {* Sign.parent_path *}
 
+hide_const (open) rel
+
 syntax
   -- {* list Enumeration *}
   "_list" :: "args => 'a list"    ("[(_)]")