Adapted to new package for inductive sets.

Inserted definition of in_rel again (since member2 was removed).

Added ML bindings for sup_fun_eq and sup_bool_eq.

top and bot are now constants.

Renamed inductive2 to inductive.

acc is now defined using inductive_set.

Added new package for inductive sets.

Adapted to new inductive definition package.

Adapted to changes in inductive definition package.

tuned comment markup;

treat OuterLex.Error;

separated Malformed (symbolic char) from Error (bad input); unparse: Output.escape_malformed; name_of: use unparse;

Output.escape_malformed;

added escape_malformed (failsafe);

Basic editing of theory sources.

tuned;

export html_mode, begin_document, end_document;

renamed XML.Rawtext to XML.Output;

export get_lexicons;

added kind_of; unparse: extra care for Malformed;

Markup.enclose;

more markup for inner and outer syntax; added enclose;

simplified funpow, untabify;

added Thy/thy_edit.ML;

added some markup for outer syntax;

clarified merge of module names

now a monolithic module

now works with SML/NJ

tuned

improvement for code names

removed proof dependency on transitivity theorems

moved lfp_induct2 here

clarified import

moved lfp_induct2 to Relation.thy

moved some finite lemmas here

moved finite lemmas to Finite_Set.thy

added print_mode setup (from pretty.ML); removed no_state;

Markup.add_mode;

removed no_state markup -- produce empty state; Markup.add_mode;

Markup.output; removed no_state markup -- produce empty state;

moved source cascading from scan.ML to source.ML;

infixr || (more efficient); tuned signature; removed unused trace'; moved source cascading from scan.ML to source.ML; tuned;

moved print_mode setup for markup to markup.ML;

Markup.output;

use position.ML earlier;

Add widthN to signature

cd ISABELLE_HOME/etc;

adjusted

updated keywords

simplified, tuned

re-expanded paths

replaced code generator framework for reflected cooper

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;

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;