scan: changed treatment of malformed symbols, passed to next stage; tuned sym_explode;

nested source: error msg passed to recover;

tuned signature; nested source: error msg passed to recover;

replaced name by file (unquoted); str_of: markup; misc cleanup;

moved Path.position to Position.path;

proper position markup; added properties operation; tuned;

use position.ML after pretty.ML;

removed target RAW-ProofGeneral (impractical to maintain);

declare: disallow quote (") in names;

removed legacy ML file; fixed prems_conv;

HOL-Complex-Matrix: fixed deps -- sort of;

adopted to new computing oracle and fixed bugs introduced by tuning

added computing oracle support for HOL and numerals

new version of computing oracle

simplified writeln_fn;

prompt: plain string, not output;

type output = string indicates raw system output;

symbolic output: avoid empty blocks, 1 space for fbreak;

tuned;

thm tag: Markup.property list;

gensym: slightly more obscure prefix descreases probability of name clash;

replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;

attribute tagged: single argument;

updated;

simplified Symtab;

renamed ML_exc to ML_exn;

Show the use of reflection attribute; fixed comments about the order of absorbing equations : f (C x) = x ; now automaically tried as last;

Changed syntax for the reflection method (reify unchanged). reflection takes an optional set of theorems for reification then several correctness theorems are specified by rules:'' then the optional term is specified by only:

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;

renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac; simplified ObjectLogic.atomize;

simplified ObjectLogic.atomize;

renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;

Revert body of pgml to match schema for now [change bad for Broker]

Classify -- comments as ordinary comments (no undo)

tuned;

avoid polymorphic equality; added dest_judgment;

sort_le: tuned eq case;

tuned goal conversion interfaces;

else_conv: only handle THM | CTERM | TERM | TYPE; prems_conv: no index; renamed goal_conv_rule to gconv_rule;

avoid polymorphic equality; Numeral.mk_cnumber;

tuned;