src/HOL/SetInterval.thy
changeset 19376 529b735edbf2
parent 19106 6e6b5b1fdc06
child 19469 958d2f2dd8d4
     1.1 --- a/src/HOL/SetInterval.thy	Sat Apr 08 22:51:35 2006 +0200
     1.2 +++ b/src/HOL/SetInterval.thy	Sun Apr 09 14:20:23 2006 +0200
     1.3 @@ -38,7 +38,7 @@
     1.4    atLeastAtMost :: "['a::ord, 'a] => 'a set"        ("(1{_.._})")
     1.5    "{l..u} == {l..} Int {..u}"
     1.6  
     1.7 -(* Old syntax, will disappear! *)
     1.8 +(* Old syntax, no longer supported:
     1.9  syntax
    1.10    "_lessThan"    :: "('a::ord) => 'a set"	("(1{.._'(})")
    1.11    "_greaterThan" :: "('a::ord) => 'a set"	("(1{')_..})")
    1.12 @@ -51,7 +51,7 @@
    1.13    "{)m..n(}" => "{m<..<n}"
    1.14    "{m..n(}" => "{m..<n}"
    1.15    "{)m..n}" => "{m<..n}"
    1.16 -
    1.17 +*)
    1.18  
    1.19  text{* A note of warning when using @{term"{..<n}"} on type @{typ
    1.20  nat}: it is equivalent to @{term"{0::nat..<n}"} but some lemmas involving