src/HOL/SetInterval.thy
changeset 11609 3f3d1add4d94
parent 10214 77349ed89f45
child 13735 7de9342aca7a
     1.1 --- a/src/HOL/SetInterval.thy	Thu Sep 27 22:26:00 2001 +0200
     1.2 +++ b/src/HOL/SetInterval.thy	Thu Sep 27 22:28:16 2001 +0200
     1.3 @@ -6,19 +6,19 @@
     1.4  lessThan, greaterThan, atLeast, atMost
     1.5  *)
     1.6  
     1.7 -SetInterval = equalities + NatArith + 
     1.8 +SetInterval = NatArith + 
     1.9  
    1.10  constdefs
    1.11 - lessThan    :: "('a::ord) => 'a set"	("(1{.._'(})")
    1.12 -"{..u(} == {x. x<u}"
    1.13 +  lessThan    :: "('a::ord) => 'a set"	("(1{.._'(})")
    1.14 +  "{..u(} == {x. x<u}"
    1.15  
    1.16 - atMost      :: "('a::ord) => 'a set"	("(1{.._})")
    1.17 -"{..u} == {x. x<=u}"
    1.18 +  atMost      :: "('a::ord) => 'a set"	("(1{.._})")
    1.19 +  "{..u} == {x. x<=u}"
    1.20  
    1.21 - greaterThan :: "('a::ord) => 'a set"	("(1{')_..})")
    1.22 -"{)l..} == {x. l<x}"
    1.23 +  greaterThan :: "('a::ord) => 'a set"	("(1{')_..})")
    1.24 +  "{)l..} == {x. l<x}"
    1.25  
    1.26 - atLeast     :: "('a::ord) => 'a set"	("(1{_..})")
    1.27 -"{l..} == {x. l<=x}"
    1.28 +  atLeast     :: "('a::ord) => 'a set"	("(1{_..})")
    1.29 +  "{l..} == {x. l<=x}"
    1.30  
    1.31  end