| Tue, 25 Dec 2001 10:02:20 +0100 | paulson | some new theorems | changeset | files |
| Tue, 25 Dec 2001 10:02:01 +0100 | paulson | conversion to Isar | changeset | files |
| Sat, 22 Dec 2001 19:46:16 +0100 | paulson | tweaked the standard theorems | changeset | files |
| Sat, 22 Dec 2001 19:42:35 +0100 | paulson | Resid converted to Isar/ZF | changeset | files |
| Fri, 21 Dec 2001 23:20:29 +0100 | wenzelm | restart: sync_thy_loader instead of overly aggressive touch_all_thys; | changeset | files |
| Fri, 21 Dec 2001 23:18:46 +0100 | wenzelm | qualified point.more; | changeset | files |
| Fri, 21 Dec 2001 23:18:27 +0100 | wenzelm | hide base name of "make", "fields", "extend", "truncate", "more", | changeset | files |
| Fri, 21 Dec 2001 23:17:35 +0100 | wenzelm | Theory.hide_space_i true; | changeset | files |
| Fri, 21 Dec 2001 23:17:12 +0100 | wenzelm | hide: flag for full/base name; | changeset | files |
| Fri, 21 Dec 2001 23:16:17 +0100 | wenzelm | HOL/record: shared operations ("more", "fields", etc.) now need to be | changeset | files |
| Fri, 21 Dec 2001 20:58:42 +0100 | wenzelm | tuned; | changeset | files |
| Fri, 21 Dec 2001 20:58:25 +0100 | wenzelm | updated; | changeset | files |
| Fri, 21 Dec 2001 19:56:42 +0100 | wenzelm | updated; | changeset | files |
| Fri, 21 Dec 2001 19:56:19 +0100 | wenzelm | isatool browser -o; | changeset | files |
| Fri, 21 Dec 2001 19:55:39 +0100 | wenzelm | removed Misc/Translations (text covered by Documents.thy); | changeset | files |
| Fri, 21 Dec 2001 17:31:45 +0100 | berghofe | Redundant patterns no longer cause errors. | changeset | files |
| Fri, 21 Dec 2001 17:31:08 +0100 | berghofe | Code generator now adds type constraints to val declarations (to make | changeset | files |
| Fri, 21 Dec 2001 15:18:07 +0100 | wenzelm | tuned; | changeset | files |
| Fri, 21 Dec 2001 00:44:35 +0100 | wenzelm | updated; | changeset | files |
| Fri, 21 Dec 2001 00:43:58 +0100 | wenzelm | removed Types/records.tex; | changeset | files |
| Fri, 21 Dec 2001 00:40:52 +0100 | wenzelm | added add_fixes: derives mssing type scheme from mixfix; | changeset | files |
| Fri, 21 Dec 2001 00:40:16 +0100 | wenzelm | fixed inst_thm: proper domain of env; | changeset | files |
| Fri, 21 Dec 2001 00:38:04 +0100 | wenzelm | tuned; | changeset | files |
| Thu, 20 Dec 2001 21:15:37 +0100 | wenzelm | added lemma; | changeset | files |
| Thu, 20 Dec 2001 21:14:59 +0100 | wenzelm | generated text; | changeset | files |
| Thu, 20 Dec 2001 21:14:42 +0100 | wenzelm | supplanted by Records.thy; | changeset | files |
| Thu, 20 Dec 2001 21:13:36 +0100 | wenzelm | some text; | changeset | files |
| Thu, 20 Dec 2001 21:13:22 +0100 | wenzelm | \usepackage{marvosym}; | changeset | files |