| changeset 10212 | 33fe2d701ddd |
| parent 8957 | 26b6e8f43305 |
| child 10214 | 77349ed89f45 |
--- a/src/HOL/SetInterval.thy Thu Oct 12 18:09:06 2000 +0200 +++ b/src/HOL/SetInterval.thy Thu Oct 12 18:38:23 2000 +0200 @@ -6,7 +6,7 @@ lessThan, greaterThan, atLeast, atMost *) -SetInterval = equalities + Arith + +SetInterval = equalities + Arithmetic + constdefs lessThan :: "('a::ord) => 'a set" ("(1{.._'(})")