35 greaterThanAtMost :: "['a::ord, 'a] => 'a set" ("(1{_<.._})") |
35 greaterThanAtMost :: "['a::ord, 'a] => 'a set" ("(1{_<.._})") |
36 "{l<..u} == {l<..} Int {..u}" |
36 "{l<..u} == {l<..} Int {..u}" |
37 |
37 |
38 atLeastAtMost :: "['a::ord, 'a] => 'a set" ("(1{_.._})") |
38 atLeastAtMost :: "['a::ord, 'a] => 'a set" ("(1{_.._})") |
39 "{l..u} == {l..} Int {..u}" |
39 "{l..u} == {l..} Int {..u}" |
40 |
|
41 (* Old syntax, no longer supported: |
|
42 syntax |
|
43 "_lessThan" :: "('a::ord) => 'a set" ("(1{.._'(})") |
|
44 "_greaterThan" :: "('a::ord) => 'a set" ("(1{')_..})") |
|
45 "_greaterThanLessThan" :: "['a::ord, 'a] => 'a set" ("(1{')_.._'(})") |
|
46 "_atLeastLessThan" :: "['a::ord, 'a] => 'a set" ("(1{_.._'(})") |
|
47 "_greaterThanAtMost" :: "['a::ord, 'a] => 'a set" ("(1{')_.._})") |
|
48 translations |
|
49 "{..m(}" => "{..<m}" |
|
50 "{)m..}" => "{m<..}" |
|
51 "{)m..n(}" => "{m<..<n}" |
|
52 "{m..n(}" => "{m..<n}" |
|
53 "{)m..n}" => "{m<..n}" |
|
54 *) |
|
55 |
40 |
56 text{* A note of warning when using @{term"{..<n}"} on type @{typ |
41 text{* A note of warning when using @{term"{..<n}"} on type @{typ |
57 nat}: it is equivalent to @{term"{0::nat..<n}"} but some lemmas involving |
42 nat}: it is equivalent to @{term"{0::nat..<n}"} but some lemmas involving |
58 @{term"{m..<n}"} may not exist in @{term"{..<n}"}-form as well. *} |
43 @{term"{m..<n}"} may not exist in @{term"{..<n}"}-form as well. *} |
59 |
44 |