| Thu, 19 Feb 2009 08:07:52 -0800 | huffman | add more ordering lemmas | file | diff | annotate |
| Tue, 17 Feb 2009 20:45:23 -0800 | huffman | add lemmas for exponentiation | file | diff | annotate |
| Mon, 16 Feb 2009 19:35:52 -0800 | huffman | tune section headings; add square function | file | diff | annotate |
| Mon, 16 Feb 2009 13:42:45 -0800 | huffman | merged | file | diff | annotate |
| Mon, 16 Feb 2009 13:42:15 -0800 | huffman | rearrange subsections | file | diff | annotate |
| Mon, 16 Feb 2009 13:14:36 -0800 | huffman | remove instances num::semiring and num::linorder | file | diff | annotate |
| Mon, 16 Feb 2009 13:08:21 -0800 | huffman | datatype num = One | Dig0 num | Dig1 num | file | diff | annotate |
| Mon, 16 Feb 2009 12:53:59 -0800 | huffman | replace 1::num with One; remove monoid_mult instance | file | diff | annotate |
| Sun, 15 Feb 2009 19:53:20 -0800 | huffman | replace dec with double-and-decrement function | file | diff | annotate |
| Mon, 16 Feb 2009 13:38:10 +0100 | haftmann | tuned texts | file | diff | annotate |
| Wed, 28 Jan 2009 16:29:16 +0100 | nipkow | Replaced group_ and ring_simps by algebra_simps; | file | diff | annotate |
| Mon, 17 Nov 2008 17:00:55 +0100 | haftmann | tuned unfold_locales invocation | file | diff | annotate |
| Fri, 10 Oct 2008 06:45:53 +0200 | haftmann | `code func` now just `code` | file | diff | annotate |
| Fri, 26 Sep 2008 09:09:51 +0200 | haftmann | op = vs. eq | file | diff | annotate |
| Thu, 28 Aug 2008 22:08:11 +0200 | haftmann | no parameter prefix for class interpretation | file | diff | annotate |
| Wed, 27 Aug 2008 12:01:59 +0200 | haftmann | added HOL/ex/Numeral.thy | file | diff | annotate |