Tue, 22 Sep 2009 15:36:55 +0200 | haftmann | be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer | file | diff | annotate |
Fri, 28 Aug 2009 20:18:33 +0200 | nipkow | tuned proofs | file | diff | annotate |
Fri, 28 Aug 2009 18:52:41 +0200 | nipkow | Turned "x <= y ==> sup x y = y" (and relatives) into simp rules | file | diff | annotate |