| Fri, 06 Sep 2024 13:49:43 +0200 |
wenzelm |
clarified signature and modules;
|
file |
diff |
annotate
|
| Thu, 05 Sep 2024 21:16:53 +0200 |
wenzelm |
clarified Pretty.T vs. output tree (following Isabelle/Scala): Output.output_width (via print_mode) happens during formatting, instead of construction;
|
file |
diff |
annotate
|
| Thu, 05 Sep 2024 17:39:45 +0200 |
wenzelm |
clarified signature: type ML_Pretty.pretty coincides with PolyML.pretty;
|
file |
diff |
annotate
|
| Wed, 04 Sep 2024 16:21:52 +0200 |
wenzelm |
clarified signature (see also 8bef51521f21);
|
file |
diff |
annotate
|
| Mon, 02 Sep 2024 20:54:00 +0200 |
wenzelm |
clarified modules: enable pretty.ML to use XML/YXML more directly;
|
file |
diff |
annotate
|
| Tue, 05 Dec 2023 11:11:00 +0100 |
wenzelm |
more ML pretty-printing;
|
file |
diff |
annotate
|
| Wed, 06 Sep 2023 16:03:22 +0200 |
wenzelm |
add ML_system_pp for type Isabelle_Thread.T;
|
file |
diff |
annotate
|
| Tue, 21 Apr 2020 22:19:59 +0200 |
wenzelm |
clarified signature: avoid clash with Isabelle/Scala Term.OFCLASS on case-insensible file-system;
|
file |
diff |
annotate
|
| Tue, 23 Jul 2019 12:07:50 +0200 |
wenzelm |
proof terms are always constructed sequentially;
|
file |
diff |
annotate
|
| Mon, 08 Jan 2018 22:36:02 +0100 |
wenzelm |
clarified implicit Pure.thy;
|
file |
diff |
annotate
|
| Sat, 02 Apr 2016 21:10:07 +0200 |
wenzelm |
careful export of type-dependent functions, without losing their special status;
|
file |
diff |
annotate
|
| Fri, 18 Mar 2016 21:29:10 +0100 |
wenzelm |
observe ML print depth;
|
file |
diff |
annotate
|
| Fri, 18 Mar 2016 17:51:57 +0100 |
wenzelm |
clarified Pretty.T toplevel pp;
|
file |
diff |
annotate
|
| Fri, 18 Mar 2016 16:38:40 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
| base
|