| Mon, 23 Feb 2009 16:25:52 -0800 | huffman | make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules | file | diff | annotate |
| Sat, 06 Dec 2008 19:39:53 -0800 | huffman | change lemmas to avoid using neg | file | diff | annotate |
| Wed, 03 Dec 2008 15:58:44 +0100 | haftmann | made repository layout more coherent with logical distribution structure; stripped some $Id$s | file | diff | annotate |
| Mon, 29 Sep 2008 12:31:59 +0200 | haftmann | clarified dependencies between arith tools | file | diff | annotate |
| Fri, 28 Mar 2008 19:43:54 +0100 | wenzelm | avoid rebinding of existing facts; | file | diff | annotate |
| Tue, 18 Mar 2008 20:33:28 +0100 | wenzelm | avoid rebinding of existing facts; | file | diff | annotate |
| Wed, 27 Feb 2008 14:39:48 +0100 | chaieb | Installation of Quantifier elimination for ordered fields moved to Library/Dense_Linear_Order.thy | file | diff | annotate |