tuned;

more markup elements for ML programs;

merged

process at-sml-dev last -- takes very long (why?);

fix

merged

presburger uses [arith] now

merged

merged

added Imperative_HOL_ex

Use assms rather than prems in find_theorems solves.

clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros

lemmas add_sign_intros

merged

moved Imperative_HOL examples to Imperative_HOL/ex

corrected variable renaming

tuned error messages

moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac

structure LinArith now named Lin_Arith

suddenly infix identifier oo occurs in generated code

datatype antiquote: maintain original Position.range, which is eventually attached to the resulting ML tokens;

eliminated non-canonical alias structure T = ML_Lex;

error "Static Errors";

more systematic type use_context; result_fun: actually apply result, only one version of eval; removed obsolete 'ML_parse';

tuned;

more systematic type use_context;

eliminated Output.ml_output;

pretty_ml/ml_pretty: proper handling of markup and string length;

more systematic type use_context;

removed obsolete ml_output;

more systematic type use_context; put_message: print optional context message as well;

more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;

de-camelized ML_Name_Space;

suppress status output for traditional tty modes (including Proof General); keyword report: explicitly issue message on writeln channel as well;

added report_text -- status messages with text body;

maintain parse trees cumulatively;

Block markup: maintain output version within tree values (in accordance with String) -- changes operational behaviour wrt. print_mode; to_ML/from_ML: proper handling of markup;

future scheduler: reduced wait timeout if tasks need to be canceled -- to improve reactivity of interrupts;

merged

Main is (Complex_Main) base entry point in library theories

Main is (Complex_Main) base entry point in library theories

added instances for bot, top, wellorder

tuned header

more canonical import, syntax fix

merged

merged

more antiquotations

moved import of module qelim to theory Presburger

tuned header

dropped theory Arith_Tools

lemma nat_dvd_not_less moved here from Arith_Tools

distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly

merged

merged

1. New cancellation simprocs for common factors in inequations 2. Updated the documentation

clarified relationship of modules Code_Name and Code_Printer

added Symreltab (binary relations of symbols) instance of TableFun

proper signature; eval: added do_run flag, store result parsetree if disabled; added 'ML_parse' command;

added read_antiq, with improved error reporting; tuned signature; tuned;

ML_Lex.read_antiq; eval: observe verbose flag; command 'ML_test': proper keyword classification, inherit_env;

ML_Lex.read_antiq;

simplified Antiquote.read (again);

export report -- version that actually covers all cases; export check_nesting; simplified read (again);

Test of advanced ML compiler invocation in Poly/ML 5.3.

ML/ml_test.ML: test of advanced ML compiler invocation in Poly/ML 5.3;

added pretty_ml;

export eval_antiquotes: refined version that operates on ML tokens;

ML_Lex.pos_of: regular position; added ML_Lex.text_of;

replaced Antiquote.is_antiq by Antiquote.is_text;

merged

extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;

merged

merged

move field lemmas into class locale context

move diff_eq_0_iff_eq into class locale context

removed obsolete pprint operations; some explicit pp operations for toplevel pretty printing;

added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;

adapted toplevel_pp to ML_Pretty.pretty;

replaced install_pp/make_pp by more general toplevel_pp based on use_text;

simplified datatype ML_Pretty.pretty: model Isabelle not Poly/ML; removed obsolete pprint;

simplified datatype ML_Pretty.pretty: model Isabelle not Poly/ML;

Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).

Pretty.position; try use ml_system specific install_pp;

added position; added to_ML, from_ML (approximation);

added generic ML_Pretty interface;

restricted interrupts for tasks running as future worker thread -- attempt to prevent interrupt race conditions;

more ambitious ML_OPTIONS;

more stats;

added ML syntax markup;

report markup for ML tokens;

Antiquote.read: argument for reporting text;

future_job: do not inherit attributes, but enforce restricted interrupts -- attempt to prevent interrupt race conditions;

uniform ml_prompts for RAW and Pure;

eliminated old Addsimps;

Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;

fixed possibility_tac;

eliminated global SIMPSET, CLASET etc. -- refer to explicit context;

merged

merged

split_codegen now eta-expands terms on-the-fly.

proper context for prove_cont/adm_tac;

with_attributes: canonical capture/release scheme (potentially iron out race condition);

considerable speedup of benchmarks by using minimal simpset;

allow non-printable symbols within string tokens;

merged

add lemma det_diagonal; remove wellorder requirement on several lemmas

merged

tuned some theorem and attribute bindings

proper spacing before ML antiquotations -- note that @ may be part of symbolic ML identifiers;

eval_antiquotes: joint scanning of ML tokens and antiquotations;

added scan_antiq; more robust scan_ml: plain scanning without cut, regular Symbol_Pos.content instead of Symbol_Pos.implode (which contains spurious Symbol.DEL is used with proper positions);

RAW: provide dummy Isar.main to make tty work gracefully (with ML toplevel);

added tokenize; internal scan_str: ensure Symbol.is_regular, otherwise it might swallow the stopper and crash!

parameterized datatype antiquote and read operation;

Antiquote.Text: keep full position information;

OuterLex.read_antiq;

moved Isar/antiquote.ML to General/antiquote.ML, which is loaded early;

moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML; scan_comment: recovered change_prompt; moved read_antiq to outer_lex.ML;

use Name.of_binding for basic logical entities without name space (fixes, case names etc.);

Name.of_binding: proper full_name (with checks) before projecting base name;