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