wenzelm [Sat, 07 Jul 2007 12:16:18 +0200] rev 23630
pretty: markup for syntax/name of authentic consts;
datatype symb: String (potential markup) vs. Space (no markup);
wenzelm [Sat, 07 Jul 2007 12:16:17 +0200] rev 23629
depend on alist.ML, markup.ML;
wenzelm [Sat, 07 Jul 2007 12:16:16 +0200] rev 23628
markup: emit as control information -- no indent text;
wenzelm [Sat, 07 Jul 2007 12:16:15 +0200] rev 23627
added property conversions;
tuned;
wenzelm [Sat, 07 Jul 2007 12:16:14 +0200] rev 23626
position: line and name;
tuned operations;
wenzelm [Sat, 07 Jul 2007 12:16:13 +0200] rev 23625
moved markup.ML before position.ML;
chaieb [Sat, 07 Jul 2007 11:09:40 +0200] rev 23624
The order for parameter for interpretation is now inversted:
f t env0 env1 ... envn = ...
where t is the type to be reified;
wenzelm [Sat, 07 Jul 2007 00:17:10 +0200] rev 23623
Common markup elements.
wenzelm [Sat, 07 Jul 2007 00:15:03 +0200] rev 23622
simplified pretty token metric: type int;
added command markup;
token translations: proper treatment of skolems;
separate print_mode setup for Output/Pretty;
wenzelm [Sat, 07 Jul 2007 00:15:02 +0200] rev 23621
simplified pretty token metric: type int;
separate print_mode setup for Output/Pretty;
wenzelm [Sat, 07 Jul 2007 00:15:02 +0200] rev 23620
moved General/xml.ML to Tools/xml.ML;
actually use pgml.ML;
wenzelm [Sat, 07 Jul 2007 00:15:00 +0200] rev 23619
tuned;
wenzelm [Sat, 07 Jul 2007 00:14:59 +0200] rev 23618
simplified output mode setup;
removed unused symbol_output;
tuned;
wenzelm [Sat, 07 Jul 2007 00:14:58 +0200] rev 23617
added print_mode setup: indent and markup;
simplified pretty token metric: type int;
added general markup for blocks;
removed unused writelns;
wenzelm [Sat, 07 Jul 2007 00:14:57 +0200] rev 23616
renamed raw to escape;
simplified pretty token metric: type int;
simplified print_mode setup: output_width and escape;
moved pretty setup to pretty.ML;
wenzelm [Sat, 07 Jul 2007 00:14:56 +0200] rev 23615
simplified pretty token metric: type int;
wenzelm [Sat, 07 Jul 2007 00:14:54 +0200] rev 23614
moved General/xml.ML to Tools/xml.ML;
wenzelm [Sat, 07 Jul 2007 00:14:52 +0200] rev 23613
added General/markup.ML;
moved General/xml.ML to Tools/xml.ML;
wenzelm [Sat, 07 Jul 2007 00:14:49 +0200] rev 23612
added class skolem, command;
nipkow [Fri, 06 Jul 2007 23:26:13 +0200] rev 23611
more interpretations
aspinall [Fri, 06 Jul 2007 17:52:52 +0200] rev 23610
Produce good PGML 2.0
webertj [Fri, 06 Jul 2007 17:21:18 +0200] rev 23609
cosmetic (line length fixed)
chaieb [Fri, 06 Jul 2007 16:09:28 +0200] rev 23608
Some examples for reifying type variables
chaieb [Fri, 06 Jul 2007 16:09:27 +0200] rev 23607
Tuned document
chaieb [Fri, 06 Jul 2007 16:09:26 +0200] rev 23606
Cleaned add and del attributes
chaieb [Fri, 06 Jul 2007 16:09:25 +0200] rev 23605
Reification now deals with type variables
wenzelm [Fri, 06 Jul 2007 11:55:05 +0200] rev 23604
Cumulative reports for Poly/ML profiling output.
aspinall [Thu, 05 Jul 2007 20:36:48 +0200] rev 23603
Update PGML version, add system name
wenzelm [Thu, 05 Jul 2007 20:01:39 +0200] rev 23602
tuned interfaces: atomize, atomize_prems, atomize_prems_tac;
removed atomize_cterm/goal;
wenzelm [Thu, 05 Jul 2007 20:01:38 +0200] rev 23601
added type conv;
merge_thys: removed dead exception handlers;
tuned;