| Wed, 23 Jan 2008 22:57:07 +0100 | wenzelm | recovered #der example without using val it; | changeset | files |
| Wed, 23 Jan 2008 09:57:55 +0100 | haftmann | yet another OCaml fix | changeset | files |
| Tue, 22 Jan 2008 23:07:25 +0100 | haftmann | tuned | changeset | files |
| Tue, 22 Jan 2008 23:07:24 +0100 | haftmann | added map_split | changeset | files |
| Tue, 22 Jan 2008 23:07:21 +0100 | haftmann | added class semiring_div | changeset | files |
| Tue, 22 Jan 2008 23:06:58 +0100 | haftmann | fixed OCaml | changeset | files |
| Tue, 22 Jan 2008 11:37:28 +0100 | haftmann | avoid 'it' in ML expressions | changeset | files |
| Mon, 21 Jan 2008 14:18:49 +0100 | berghofe | Removed Logic.auto_rename. | changeset | files |
| Mon, 21 Jan 2008 08:45:36 +0100 | haftmann | Efficient_Nat streamlined and improved | changeset | files |
| Mon, 21 Jan 2008 08:43:37 +0100 | haftmann | tuned proof | changeset | files |
| Mon, 21 Jan 2008 08:43:36 +0100 | haftmann | non-negative numerals | changeset | files |
| Mon, 21 Jan 2008 08:43:35 +0100 | haftmann | tuned | changeset | files |
| Mon, 21 Jan 2008 08:43:34 +0100 | haftmann | more lemmas | changeset | files |
| Mon, 21 Jan 2008 08:43:33 +0100 | haftmann | proper meaningful examples | changeset | files |
| Mon, 21 Jan 2008 08:43:32 +0100 | haftmann | explicit auxiliary function for code setup | changeset | files |
| Mon, 21 Jan 2008 08:43:31 +0100 | haftmann | streamlined and improved | changeset | files |
| Mon, 21 Jan 2008 08:43:30 +0100 | haftmann | adjusted to constant and theorem renames | changeset | files |
| Mon, 21 Jan 2008 08:43:29 +0100 | haftmann | avoiding direct references to numeral presentation | changeset | files |
| Mon, 21 Jan 2008 08:43:27 +0100 | haftmann | tuned code setup | changeset | files |
| Fri, 18 Jan 2008 20:34:28 +0100 | huffman | add space to binder syntax | changeset | files |
| Fri, 18 Jan 2008 20:31:11 +0100 | huffman | pcpodef generates strict_iff lemmas | changeset | files |
| Fri, 18 Jan 2008 20:22:07 +0100 | huffman | change lemma admD to rule_format | changeset | files |
| Fri, 18 Jan 2008 08:30:12 +0100 | haftmann | improved implementation | changeset | files |
| Thu, 17 Jan 2008 21:56:33 +0100 | huffman | convert lemma lub_mono to rule_format | changeset | files |
| Thu, 17 Jan 2008 21:44:19 +0100 | huffman | rename lemma chain_mono3 -> chain_mono, chain_mono -> chain_mono_less | changeset | files |
| Thu, 17 Jan 2008 00:51:20 +0100 | huffman | change class axiom chfin to rule_format | changeset | files |
| Wed, 16 Jan 2008 22:41:49 +0100 | huffman | change class axiom ax_flat to rule_format | changeset | files |
| Tue, 15 Jan 2008 16:19:23 +0100 | haftmann | joined theories IntDef, Numeral, IntArith to theory Int | changeset | files |
| Tue, 15 Jan 2008 16:19:21 +0100 | haftmann | tuned | changeset | files |
| Tue, 15 Jan 2008 16:19:20 +0100 | haftmann | further localization | changeset | files |