Try several correctness theorems for reflection; rearrange cong rules to avoid the absoption cases;

Context data now consist of eqations for reification and equations for correctness theorems for reflection; Added attribute reflection to store correctness theorems to be trued by default

simplified/more robust print_state; more robust prompt markup;

export mode_markup; added symbolic output (via print_mode); misc cleanup;

added markup for pretty printing;

Corrected erronus use of compiletime context to the runtime context

make smlnj happy;

toplevel prompt/print_state: proper markup, removed hooks;

toplevel prompt/print_state: proper markup, removed hooks; tuned;

pretty_state: subgoal markup; tuned;

added markup_chunks;

added toplevel markup; misc cleanup;

use markup.ML earlier;

removed obsolete disable_pr/enable_pr; added old print_goals from display.ML;

pretty_goals_aux: subgoal markup; print_goals etc.: moved old version to old_goals.ML, removed hooks; tuned;

pr_goals: adapted Display.pretty_goals_aux; pr_goals/prterm: proper context; tuned;

export attribute;

pretty_sort/typ/term: markup;

pretty: markup for syntax/name of authentic consts; datatype symb: String (potential markup) vs. Space (no markup);

depend on alist.ML, markup.ML;

markup: emit as control information -- no indent text;

added property conversions; tuned;

position: line and name; tuned operations;

moved markup.ML before position.ML;

The order for parameter for interpretation is now inversted: f t env0 env1 ... envn = ... where t is the type to be reified;

Common markup elements.

simplified pretty token metric: type int; added command markup; token translations: proper treatment of skolems; separate print_mode setup for Output/Pretty;

simplified pretty token metric: type int; separate print_mode setup for Output/Pretty;

moved General/xml.ML to Tools/xml.ML; actually use pgml.ML;

tuned;

simplified output mode setup; removed unused symbol_output; tuned;

added print_mode setup: indent and markup; simplified pretty token metric: type int; added general markup for blocks; removed unused writelns;

renamed raw to escape; simplified pretty token metric: type int; simplified print_mode setup: output_width and escape; moved pretty setup to pretty.ML;

simplified pretty token metric: type int;

moved General/xml.ML to Tools/xml.ML;

added General/markup.ML; moved General/xml.ML to Tools/xml.ML;

added class skolem, command;

more interpretations

Produce good PGML 2.0

cosmetic (line length fixed)

Some examples for reifying type variables

Tuned document

Cleaned add and del attributes

Reification now deals with type variables

Cumulative reports for Poly/ML profiling output.

Update PGML version, add system name

tuned interfaces: atomize, atomize_prems, atomize_prems_tac; removed atomize_cterm/goal;

added type conv; merge_thys: removed dead exception handlers; tuned;

removed comments -- no exception TERM; merge_list: exception THEORY;

added is_reflexive;

tuned;

simplified has_meta_prems;

moved type conv to thm.ML; renamed Conv.is_refl to Thm.is_reflexive; misc tuning of basic conversions;

the_theory/proof: error instead of exception Fail;

renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac; added flat_rule filter for addXXs etc.;

renamed Conv.is_refl to Thm.is_reflexive;