--- a/src/HOL/SetInterval.thy Tue May 02 20:42:33 2006 +0200
+++ b/src/HOL/SetInterval.thy Tue May 02 20:42:34 2006 +0200
@@ -38,21 +38,6 @@
atLeastAtMost :: "['a::ord, 'a] => 'a set" ("(1{_.._})")
"{l..u} == {l..} Int {..u}"
-(* 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{_.._'(})")
- "_greaterThanAtMost" :: "['a::ord, 'a] => 'a set" ("(1{')_.._})")
-translations
- "{..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. *}