| Fri, 17 Mar 2000 16:28:59 +0100 |
wenzelm |
untag: remove all tags of given name;
|
changeset |
files
|
| Fri, 17 Mar 2000 16:27:28 +0100 |
wenzelm |
no begin_goal marker (interferes with "latex" etc. output; useless anyway?)
|
changeset |
files
|
| Fri, 17 Mar 2000 16:26:43 +0100 |
wenzelm |
next_block: allow in non-goal blocks as well (experimental);
|
changeset |
files
|
| Fri, 17 Mar 2000 15:51:13 +0100 |
paulson |
re-ordered the theorems
|
changeset |
files
|
| Fri, 17 Mar 2000 15:49:50 +0100 |
paulson |
better error messages, especially for multiple types
|
changeset |
files
|
| Thu, 16 Mar 2000 00:36:22 +0100 |
wenzelm |
Splitter support;
|
changeset |
files
|
| Thu, 16 Mar 2000 00:35:27 +0100 |
wenzelm |
added HOL/PreLIst.thy;
|
changeset |
files
|
| Thu, 16 Mar 2000 00:33:46 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 16 Mar 2000 00:32:55 +0100 |
wenzelm |
do not change parindent/parskip;
|
changeset |
files
|
| Thu, 16 Mar 2000 00:31:58 +0100 |
wenzelm |
Isar: splitter support; improved diagnostics;
|
changeset |
files
|
| Thu, 16 Mar 2000 00:29:03 +0100 |
wenzelm |
Splitter support;
|
changeset |
files
|
| Thu, 16 Mar 2000 00:28:35 +0100 |
wenzelm |
moved "cases" to generic.tex;
|
changeset |
files
|