Sat, 07 Jul 2007 00:15:02 +0200 moved General/xml.ML to Tools/xml.ML;
wenzelm [Sat, 07 Jul 2007 00:15:02 +0200] rev 23620
moved General/xml.ML to Tools/xml.ML; actually use pgml.ML;
Sat, 07 Jul 2007 00:15:00 +0200 tuned;
wenzelm [Sat, 07 Jul 2007 00:15:00 +0200] rev 23619
tuned;
Sat, 07 Jul 2007 00:14:59 +0200 simplified output mode setup;
wenzelm [Sat, 07 Jul 2007 00:14:59 +0200] rev 23618
simplified output mode setup; removed unused symbol_output; tuned;
Sat, 07 Jul 2007 00:14:58 +0200 added print_mode setup: indent and markup;
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;
Sat, 07 Jul 2007 00:14:57 +0200 renamed raw to escape;
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;
Sat, 07 Jul 2007 00:14:56 +0200 simplified pretty token metric: type int;
wenzelm [Sat, 07 Jul 2007 00:14:56 +0200] rev 23615
simplified pretty token metric: type int;
Sat, 07 Jul 2007 00:14:54 +0200 moved General/xml.ML to Tools/xml.ML;
wenzelm [Sat, 07 Jul 2007 00:14:54 +0200] rev 23614
moved General/xml.ML to Tools/xml.ML;
Sat, 07 Jul 2007 00:14:52 +0200 added General/markup.ML;
wenzelm [Sat, 07 Jul 2007 00:14:52 +0200] rev 23613
added General/markup.ML; moved General/xml.ML to Tools/xml.ML;
Sat, 07 Jul 2007 00:14:49 +0200 added class skolem, command;
wenzelm [Sat, 07 Jul 2007 00:14:49 +0200] rev 23612
added class skolem, command;
Fri, 06 Jul 2007 23:26:13 +0200 more interpretations
nipkow [Fri, 06 Jul 2007 23:26:13 +0200] rev 23611
more interpretations
Fri, 06 Jul 2007 17:52:52 +0200 Produce good PGML 2.0
aspinall [Fri, 06 Jul 2007 17:52:52 +0200] rev 23610
Produce good PGML 2.0
Fri, 06 Jul 2007 17:21:18 +0200 cosmetic (line length fixed)
webertj [Fri, 06 Jul 2007 17:21:18 +0200] rev 23609
cosmetic (line length fixed)
Fri, 06 Jul 2007 16:09:28 +0200 Some examples for reifying type variables
chaieb [Fri, 06 Jul 2007 16:09:28 +0200] rev 23608
Some examples for reifying type variables
Fri, 06 Jul 2007 16:09:27 +0200 Tuned document
chaieb [Fri, 06 Jul 2007 16:09:27 +0200] rev 23607
Tuned document
Fri, 06 Jul 2007 16:09:26 +0200 Cleaned add and del attributes
chaieb [Fri, 06 Jul 2007 16:09:26 +0200] rev 23606
Cleaned add and del attributes
Fri, 06 Jul 2007 16:09:25 +0200 Reification now deals with type variables
chaieb [Fri, 06 Jul 2007 16:09:25 +0200] rev 23605
Reification now deals with type variables
Fri, 06 Jul 2007 11:55:05 +0200 Cumulative reports for Poly/ML profiling output.
wenzelm [Fri, 06 Jul 2007 11:55:05 +0200] rev 23604
Cumulative reports for Poly/ML profiling output.
Thu, 05 Jul 2007 20:36:48 +0200 Update PGML version, add system name
aspinall [Thu, 05 Jul 2007 20:36:48 +0200] rev 23603
Update PGML version, add system name
Thu, 05 Jul 2007 20:01:39 +0200 tuned interfaces: atomize, atomize_prems, atomize_prems_tac;
wenzelm [Thu, 05 Jul 2007 20:01:39 +0200] rev 23602
tuned interfaces: atomize, atomize_prems, atomize_prems_tac; removed atomize_cterm/goal;
Thu, 05 Jul 2007 20:01:38 +0200 added type conv;
wenzelm [Thu, 05 Jul 2007 20:01:38 +0200] rev 23601
added type conv; merge_thys: removed dead exception handlers; tuned;
Thu, 05 Jul 2007 20:01:37 +0200 removed comments -- no exception TERM;
wenzelm [Thu, 05 Jul 2007 20:01:37 +0200] rev 23600
removed comments -- no exception TERM; merge_list: exception THEORY;
Thu, 05 Jul 2007 20:01:36 +0200 added is_reflexive;
wenzelm [Thu, 05 Jul 2007 20:01:36 +0200] rev 23599
added is_reflexive;
Thu, 05 Jul 2007 20:01:35 +0200 tuned;
wenzelm [Thu, 05 Jul 2007 20:01:35 +0200] rev 23598
tuned;
Thu, 05 Jul 2007 20:01:34 +0200 simplified has_meta_prems;
wenzelm [Thu, 05 Jul 2007 20:01:34 +0200] rev 23597
simplified has_meta_prems;
Thu, 05 Jul 2007 20:01:33 +0200 moved type conv to thm.ML;
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;
Thu, 05 Jul 2007 20:01:32 +0200 the_theory/proof: error instead of exception Fail;
wenzelm [Thu, 05 Jul 2007 20:01:32 +0200] rev 23595
the_theory/proof: error instead of exception Fail;
Thu, 05 Jul 2007 20:01:31 +0200 renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
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.;
Thu, 05 Jul 2007 20:01:30 +0200 renamed Conv.is_refl to Thm.is_reflexive;
wenzelm [Thu, 05 Jul 2007 20:01:30 +0200] rev 23593
renamed Conv.is_refl to Thm.is_reflexive;
(0) -10000 -3000 -1000 -300 -100 -50 -28 +28 +50 +100 +300 +1000 +3000 +10000 +30000 tip