| Sat, 07 Jul 2007 18:39:16 +0200 |
wenzelm |
use markup.ML earlier;
|
changeset |
files
|
| Sat, 07 Jul 2007 18:39:15 +0200 |
wenzelm |
removed obsolete disable_pr/enable_pr;
|
changeset |
files
|
| Sat, 07 Jul 2007 18:39:14 +0200 |
wenzelm |
pretty_goals_aux: subgoal markup;
|
changeset |
files
|
| Sat, 07 Jul 2007 18:39:12 +0200 |
wenzelm |
pr_goals: adapted Display.pretty_goals_aux;
|
changeset |
files
|
| Sat, 07 Jul 2007 12:16:20 +0200 |
wenzelm |
export attribute;
|
changeset |
files
|
| Sat, 07 Jul 2007 12:16:19 +0200 |
wenzelm |
pretty_sort/typ/term: markup;
|
changeset |
files
|
| Sat, 07 Jul 2007 12:16:18 +0200 |
wenzelm |
pretty: markup for syntax/name of authentic consts;
|
changeset |
files
|
| Sat, 07 Jul 2007 12:16:17 +0200 |
wenzelm |
depend on alist.ML, markup.ML;
|
changeset |
files
|
| Sat, 07 Jul 2007 12:16:16 +0200 |
wenzelm |
markup: emit as control information -- no indent text;
|
changeset |
files
|
| Sat, 07 Jul 2007 12:16:15 +0200 |
wenzelm |
added property conversions;
|
changeset |
files
|
| Sat, 07 Jul 2007 12:16:14 +0200 |
wenzelm |
position: line and name;
|
changeset |
files
|
| Sat, 07 Jul 2007 12:16:13 +0200 |
wenzelm |
moved markup.ML before position.ML;
|
changeset |
files
|
| Sat, 07 Jul 2007 11:09:40 +0200 |
chaieb |
The order for parameter for interpretation is now inversted:
|
changeset |
files
|
| Sat, 07 Jul 2007 00:17:10 +0200 |
wenzelm |
Common markup elements.
|
changeset |
files
|
| Sat, 07 Jul 2007 00:15:03 +0200 |
wenzelm |
simplified pretty token metric: type int;
|
changeset |
files
|