| Mon, 20 Aug 2007 17:46:32 +0200 |
wenzelm |
type_check: tuned singleton funs case;
|
changeset |
files
|
| Mon, 20 Aug 2007 17:46:31 +0200 |
wenzelm |
theory header: more precise imports;
|
changeset |
files
|
| Mon, 20 Aug 2007 17:34:04 +0200 |
huffman |
Word/document/root.tex
|
changeset |
files
|
| Mon, 20 Aug 2007 17:31:59 +0200 |
huffman |
new root.tex for HOL-Word
|
changeset |
files
|
| Mon, 20 Aug 2007 17:31:01 +0200 |
huffman |
no_document for Infinite_Set, Parity
|
changeset |
files
|
| Mon, 20 Aug 2007 11:18:18 +0200 |
nipkow |
removed allpairs
|
changeset |
files
|
| Mon, 20 Aug 2007 11:18:07 +0200 |
nipkow |
removed allpairs - use list comprehension!
|
changeset |
files
|
| Mon, 20 Aug 2007 04:44:35 +0200 |
kleing |
added header
|
changeset |
files
|
| Mon, 20 Aug 2007 04:34:31 +0200 |
kleing |
* HOL-Word:
|
changeset |
files
|
| Mon, 20 Aug 2007 00:22:18 +0200 |
kleing |
boolean algebras as locales and numbers as types by Brian Huffman
|
changeset |
files
|
| Sun, 19 Aug 2007 21:21:37 +0200 |
nipkow |
Made UN_Un simp
|
changeset |
files
|
| Sun, 19 Aug 2007 12:43:05 +0200 |
aspinall |
Use 376/377 specials for sendback markup
|
changeset |
files
|
| Sat, 18 Aug 2007 21:27:52 +0200 |
wenzelm |
ML system provides get_print_depth;
|
changeset |
files
|
| Sat, 18 Aug 2007 19:25:28 +0200 |
webertj |
fixed a bug in demult: -a in (-a * b) is no longer treated as atomic
|
changeset |
files
|
| Sat, 18 Aug 2007 17:42:39 +0200 |
wenzelm |
removed obsolete ML bindings;
|
changeset |
files
|