# HG changeset patch
# User nipkow
# Date 1190708863 -7200
# Node ID 9800a76026291a8c95be28177d9243742d3c9b2d
# Parent  b37d3980da3c16f1c16eaec61bd195482c9f225e
hide successor

diff -r b37d3980da3c -r 9800a7602629 src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Sep 24 22:00:18 2007 +0200
+++ b/src/HOL/List.thy	Tue Sep 25 10:27:43 2007 +0200
@@ -2596,6 +2596,8 @@
 
 text{* Now @{term"[i..j::int]"} is defined for integers. *}
 
+hide (open) const successor
+
 
 subsubsection {* @{text lists}: the list-forming operator over sets *}