src/HOL/SetInterval.thy
changeset 26072 f65a7fa2da6c
parent 25919 8b1c0d434824
child 26105 ae06618225ec
     1.1 --- a/src/HOL/SetInterval.thy	Fri Feb 15 16:09:10 2008 +0100
     1.2 +++ b/src/HOL/SetInterval.thy	Fri Feb 15 16:09:12 2008 +0100
     1.3 @@ -122,8 +122,7 @@
     1.4  
     1.5  lemma Compl_greaterThan [simp]:
     1.6      "!!k:: 'a::linorder. -greaterThan k = atMost k"
     1.7 -apply (simp add: greaterThan_def atMost_def le_def, auto)
     1.8 -done
     1.9 +  by (auto simp add: greaterThan_def atMost_def)
    1.10  
    1.11  lemma Compl_atMost [simp]: "!!k:: 'a::linorder. -atMost k = greaterThan k"
    1.12  apply (subst Compl_greaterThan [symmetric])
    1.13 @@ -135,8 +134,7 @@
    1.14  
    1.15  lemma Compl_atLeast [simp]:
    1.16      "!!k:: 'a::linorder. -atLeast k = lessThan k"
    1.17 -apply (simp add: lessThan_def atLeast_def le_def, auto)
    1.18 -done
    1.19 +  by (auto simp add: lessThan_def atLeast_def)
    1.20  
    1.21  lemma (in ord) atMost_iff [iff]: "(i: atMost k) = (i<=k)"
    1.22  by (simp add: atMost_def)