src/HOL/SetInterval.thy
changeset 19538 ae6d01fa2d8a
parent 19469 958d2f2dd8d4
child 20217 25b068a99d2b
     1.1 --- a/src/HOL/SetInterval.thy	Tue May 02 20:42:33 2006 +0200
     1.2 +++ b/src/HOL/SetInterval.thy	Tue May 02 20:42:34 2006 +0200
     1.3 @@ -38,21 +38,6 @@
     1.4    atLeastAtMost :: "['a::ord, 'a] => 'a set"        ("(1{_.._})")
     1.5    "{l..u} == {l..} Int {..u}"
     1.6  
     1.7 -(* Old syntax, no longer supported:
     1.8 -syntax
     1.9 -  "_lessThan"    :: "('a::ord) => 'a set"	("(1{.._'(})")
    1.10 -  "_greaterThan" :: "('a::ord) => 'a set"	("(1{')_..})")
    1.11 -  "_greaterThanLessThan" :: "['a::ord, 'a] => 'a set"  ("(1{')_.._'(})")
    1.12 -  "_atLeastLessThan" :: "['a::ord, 'a] => 'a set"      ("(1{_.._'(})")
    1.13 -  "_greaterThanAtMost" :: "['a::ord, 'a] => 'a set"    ("(1{')_.._})")
    1.14 -translations
    1.15 -  "{..m(}" => "{..<m}"
    1.16 -  "{)m..}" => "{m<..}"
    1.17 -  "{)m..n(}" => "{m<..<n}"
    1.18 -  "{m..n(}" => "{m..<n}"
    1.19 -  "{)m..n}" => "{m<..n}"
    1.20 -*)
    1.21 -
    1.22  text{* A note of warning when using @{term"{..<n}"} on type @{typ
    1.23  nat}: it is equivalent to @{term"{0::nat..<n}"} but some lemmas involving
    1.24  @{term"{m..<n}"} may not exist in @{term"{..<n}"}-form as well. *}