src/HOL/SetInterval.thy

   "{l<..u} == {l<..} Int {..u}"
 
   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{')_..})")
   "_greaterThanLessThan" :: "['a::ord, 'a] => 'a set"  ("(1{')_.._'(})")
   "_atLeastLessThan" :: "['a::ord, 'a] => 'a set"      ("(1{_.._'(})")

   "{..m(}" => "{..<m}"
   "{)m..}" => "{m<..}"
   "{)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
 @{term"{m..<n}"} may not exist in @{term"{..<n}"}-form as well. *}