| Tue, 13 Dec 2011 12:05:47 +0100 | huffman | remove some unwanted numeral-representation-specific simp rules | changeset | files |
| Tue, 13 Dec 2011 11:48:59 +0100 | huffman | remove redundant lemmas | changeset | files |
| Tue, 13 Dec 2011 11:26:10 +0100 | huffman | reorder some definitions and proofs, in preparation for new numeral representation | changeset | files |
| Tue, 13 Dec 2011 23:22:27 +0100 | wenzelm | merged | changeset | files |
| Tue, 13 Dec 2011 22:44:16 +0100 | noschinl | added lemmas | changeset | files |
| Tue, 13 Dec 2011 21:15:38 +0100 | nipkow | added concrete syntax | changeset | files |
| Tue, 13 Dec 2011 23:23:51 +0100 | wenzelm | 'datatype' specifications allow explicit sort constraints; | changeset | files |
| Tue, 13 Dec 2011 20:29:59 +0100 | wenzelm | do not open ML structures; | changeset | files |
| Tue, 13 Dec 2011 20:10:36 +0100 | wenzelm | tuned; | changeset | files |
| Tue, 13 Dec 2011 20:10:28 +0100 | wenzelm | removed dead code; | changeset | files |
| Tue, 13 Dec 2011 20:10:11 +0100 | wenzelm | comment; | changeset | files |
| Tue, 13 Dec 2011 16:53:28 +0100 | nipkow | connect while_option with lfp | changeset | files |