| Sat, 17 Feb 2007 17:19:59 +0100 |
aspinall |
pretty_full_theory: expose in signature.
|
file |
diff |
annotate
|
| Fri, 19 Jan 2007 22:08:02 +0100 |
wenzelm |
moved ML context stuff to from Context to ML_Context;
|
file |
diff |
annotate
|
| Fri, 19 Jan 2007 13:09:33 +0100 |
wenzelm |
adapted ML context operations;
|
file |
diff |
annotate
|
| Tue, 21 Nov 2006 18:07:33 +0100 |
wenzelm |
moved theorem kinds from PureThy to Thm;
|
file |
diff |
annotate
|
| Sat, 07 Oct 2006 01:31:17 +0200 |
wenzelm |
added pretty_consts (from specification.ML);
|
file |
diff |
annotate
|
| Tue, 19 Sep 2006 23:15:26 +0200 |
wenzelm |
'print_theory': bang option for full verbosity;
|
file |
diff |
annotate
|
| Wed, 02 Aug 2006 22:27:05 +0200 |
wenzelm |
moved debug option to proof_display.ML (again);
|
file |
diff |
annotate
|
| Sat, 29 Jul 2006 00:51:36 +0200 |
wenzelm |
rename legacy_pretty_thm to pretty_thm_legacy;
|
file |
diff |
annotate
|
| Thu, 27 Jul 2006 13:43:13 +0200 |
wenzelm |
ProofContext.legacy_pretty_thm;
|
file |
diff |
annotate
|
| Wed, 26 Jul 2006 00:44:49 +0200 |
wenzelm |
moved pprint functions to Isar/proof_display.ML;
|
file |
diff |
annotate
|
| Thu, 27 Apr 2006 15:06:35 +0200 |
wenzelm |
tuned basic list operators (flat, maps, map_filter);
|
file |
diff |
annotate
|
| Thu, 13 Apr 2006 12:01:10 +0200 |
wenzelm |
added print_theorems/theory, print_theorems_diff (from pure_thy.ML);
|
file |
diff |
annotate
|
| Fri, 27 Jan 2006 19:03:02 +0100 |
wenzelm |
moved theorem tags from Drule to PureThy;
|
file |
diff |
annotate
|
| Tue, 04 Oct 2005 19:01:37 +0200 |
wenzelm |
minor tweaks for Poplog/ML;
|
file |
diff |
annotate
|
| Tue, 13 Sep 2005 22:19:54 +0200 |
wenzelm |
Printing of Isar proof elements etc.
|
file |
diff |
annotate
|