| 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 |
| Tue, 15 Jan 2008 16:19:19 +0100 | haftmann | explicit code lemma for implication | changeset | files |
| Tue, 15 Jan 2008 02:38:13 +0100 | huffman | add instance for class bifinite | changeset | files |
| Tue, 15 Jan 2008 02:20:47 +0100 | huffman | clean up some proofs; | changeset | files |
| Tue, 15 Jan 2008 02:18:01 +0100 | huffman | declare cpair_strict [simp] | changeset | files |
| Mon, 14 Jan 2008 23:19:28 +0100 | isatest | make at-sml-dev experimental | changeset | files |
| Mon, 14 Jan 2008 21:42:58 +0100 | huffman | added bifinite class instance | changeset | files |
| Mon, 14 Jan 2008 21:16:06 +0100 | huffman | add bifinite instances | changeset | files |
| Mon, 14 Jan 2008 21:15:20 +0100 | huffman | add class bifinite_cpo for possibly-unpointed bifinite domains | changeset | files |