| Sat, 23 Jun 2007 19:33:22 +0200 | nipkow | tuned and renamed group_eq_simps and ring_eq_simps | file | diff | annotate |
| Thu, 14 Jun 2007 18:33:31 +0200 | wenzelm | tuned proofs: avoid implicit prems; | file | diff | annotate |
| Mon, 11 Jun 2007 07:10:06 +0200 | huffman | remove references to constant int::nat=>int | file | diff | annotate |
| Sat, 19 May 2007 04:52:24 +0200 | huffman | remove dependence on Hilbert_Choice.thy | file | diff | annotate |
| Fri, 18 May 2007 16:13:07 +0200 | huffman | avoid using real_mult_inverse_left; cleaned up | file | diff | annotate |
| Thu, 17 May 2007 21:51:32 +0200 | huffman | avoid using redundant lemmas from RealDef.thy | file | diff | annotate |
| Fri, 17 Nov 2006 02:20:03 +0100 | wenzelm | more robust syntax for definition/abbreviation/notation; | file | diff | annotate |