# HG changeset patch
# User nipkow
# Date 1144585223 -7200
# Node ID 529b735edbf29f27bcfb176919f923e846f1c10b
# Parent  8198a4ffff24d26b437224c4c6845a2340c7027f
Removed old set interval syntax.

diff -r 8198a4ffff24 -r 529b735edbf2 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Sat Apr 08 22:51:35 2006 +0200
+++ b/src/HOL/SetInterval.thy	Sun Apr 09 14:20:23 2006 +0200
@@ -38,7 +38,7 @@
   atLeastAtMost :: "['a::ord, 'a] => 'a set"        ("(1{_.._})")
   "{l..u} == {l..} Int {..u}"
 
-(* Old syntax, will disappear! *)
+(* Old syntax, no longer supported:
 syntax
   "_lessThan"    :: "('a::ord) => 'a set"	("(1{.._'(})")
   "_greaterThan" :: "('a::ord) => 'a set"	("(1{')_..})")
@@ -51,7 +51,7 @@
   "{)m..n(}" => "{m<..<n}"
   "{m..n(}" => "{m..<n}"
   "{)m..n}" => "{m<..n}"
-
+*)
 
 text{* A note of warning when using @{term"{..<n}"} on type @{typ
 nat}: it is equivalent to @{term"{0::nat..<n}"} but some lemmas involving