Removed old set interval syntax.
authornipkow
Sun, 09 Apr 2006 14:20:23 +0200
changeset 19376 529b735edbf2
parent 19375 8198a4ffff24
child 19377 1f717bd6b7ea
Removed old set interval syntax.
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