expanded fragile proof

extended - convers now basic lcm properties also

constant dvd now in class target

moved lemma zdvd_period here

introduced (auxiliary) class dvd_mod for more convenient code generation

tuned;

nested source: explicit interactive flag for recover avoids duplicate errors;

tuned dead code;

use Position.file_of; removed strange comments;

toplevel_source: interactive flag indicates intermittent error_msg; nested source: error msg passed to recover; tuned source positions;

Malformed token: error msg; scan: explicit handling of malformed symbols from previous stage; source: interactive flag indicates intermittent error_msg; tuned;

adapted OuterLex/T.source;

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;