wenzelm [Sat, 07 Jul 2007 18:39:17 +0200] rev 23637
added toplevel markup;
misc cleanup;
wenzelm [Sat, 07 Jul 2007 18:39:16 +0200] rev 23636
use markup.ML earlier;
wenzelm [Sat, 07 Jul 2007 18:39:15 +0200] rev 23635
removed obsolete disable_pr/enable_pr;
added old print_goals from display.ML;
wenzelm [Sat, 07 Jul 2007 18:39:14 +0200] rev 23634
pretty_goals_aux: subgoal markup;
print_goals etc.: moved old version to old_goals.ML, removed hooks;
tuned;
wenzelm [Sat, 07 Jul 2007 18:39:12 +0200] rev 23633
pr_goals: adapted Display.pretty_goals_aux;
pr_goals/prterm: proper context;
tuned;
wenzelm [Sat, 07 Jul 2007 12:16:20 +0200] rev 23632
export attribute;
wenzelm [Sat, 07 Jul 2007 12:16:19 +0200] rev 23631
pretty_sort/typ/term: markup;
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;
wenzelm [Thu, 05 Jul 2007 20:01:37 +0200] rev 23600
removed comments -- no exception TERM;
merge_list: exception THEORY;
wenzelm [Thu, 05 Jul 2007 20:01:36 +0200] rev 23599
added is_reflexive;
wenzelm [Thu, 05 Jul 2007 20:01:35 +0200] rev 23598
tuned;
wenzelm [Thu, 05 Jul 2007 20:01:34 +0200] rev 23597
simplified has_meta_prems;
wenzelm [Thu, 05 Jul 2007 20:01:33 +0200] rev 23596
moved type conv to thm.ML;
renamed Conv.is_refl to Thm.is_reflexive;
misc tuning of basic conversions;
wenzelm [Thu, 05 Jul 2007 20:01:32 +0200] rev 23595
the_theory/proof: error instead of exception Fail;
wenzelm [Thu, 05 Jul 2007 20:01:31 +0200] rev 23594
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
added flat_rule filter for addXXs etc.;
wenzelm [Thu, 05 Jul 2007 20:01:30 +0200] rev 23593
renamed Conv.is_refl to Thm.is_reflexive;
wenzelm [Thu, 05 Jul 2007 20:01:29 +0200] rev 23592
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
simplified ObjectLogic.atomize;
wenzelm [Thu, 05 Jul 2007 20:01:28 +0200] rev 23591
simplified ObjectLogic.atomize;
wenzelm [Thu, 05 Jul 2007 20:01:26 +0200] rev 23590
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
aspinall [Thu, 05 Jul 2007 19:59:01 +0200] rev 23589
Revert body of pgml to match schema for now [change bad for Broker]
aspinall [Thu, 05 Jul 2007 19:57:19 +0200] rev 23588
Classify -- comments as ordinary comments (no undo)
wenzelm [Thu, 05 Jul 2007 00:15:44 +0200] rev 23587
tuned;
wenzelm [Thu, 05 Jul 2007 00:06:25 +0200] rev 23586
avoid polymorphic equality;
added dest_judgment;
wenzelm [Thu, 05 Jul 2007 00:06:24 +0200] rev 23585
sort_le: tuned eq case;
wenzelm [Thu, 05 Jul 2007 00:06:23 +0200] rev 23584
tuned goal conversion interfaces;
wenzelm [Thu, 05 Jul 2007 00:06:22 +0200] rev 23583
else_conv: only handle THM | CTERM | TERM | TYPE;
prems_conv: no index;
renamed goal_conv_rule to gconv_rule;
wenzelm [Thu, 05 Jul 2007 00:06:20 +0200] rev 23582
avoid polymorphic equality;
Numeral.mk_cnumber;