changeset 10214 | 77349ed89f45 |
parent 10212 | 33fe2d701ddd |
child 11609 | 3f3d1add4d94 |
--- a/src/HOL/SetInterval.thy Thu Oct 12 18:44:35 2000 +0200 +++ b/src/HOL/SetInterval.thy Fri Oct 13 08:28:21 2000 +0200 @@ -6,7 +6,7 @@ lessThan, greaterThan, atLeast, atMost *) -SetInterval = equalities + Arithmetic + +SetInterval = equalities + NatArith + constdefs lessThan :: "('a::ord) => 'a set" ("(1{.._'(})")