simplified Element.activate(_i): singleton version;

tuned;

added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML; tuned;

unified binding prefix terminology;

simplified roundup activation interface;

merged

merged

merged

second attempt for code_deps command

merged

corrected projection of required statement names

corrected check for additional type variables on rhs of code equations

not yet fruitful tex experiments with bounding boxes

simplified Locale.activate operations, using generic context; misc tuning;

renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;

define_prefs: removed redundant Drule.gen_all, which is already part of the norm_hhf stage of Assumption.assume;

renamed ProofContext.note_thmss_i to ProofContext.note_thmss, eliminated obsolete external version;

simplified references to facts, eliminated external note_thmss;

added map_facts_refs;

tuned;

replaced add_binds(_i) by bind_terms -- internal version only;

replaced add_binds by singleton bind_term;

simplified internal locale parameters: maintain proper name and type, instead of binding and constraint;

minor tuning;

merged

Merged.

Corrections to locale syntax.

Update explanation of locale expressions to locale reimplementation.

Comments updated.

fixed proof

merged

fps made instance of number_ring

updated keywords with polyml-experimental;

export position_of;

dropped infix union

tuned notoriously slow metis proof

merged

dropped toy example Code_Antiq

more convenient name uniqueness

normalized imports

dropped legacy goal package call

merged

merged

step towards proper pictures in dvi

merged

parameterize assoc_fold with is_numeral predicate

merged

New theorems mostly concerning infinite series.

interpretation/interpret: prefixes are mandatory by default;

interpretation/interpret: prefixes are mandatory by default; misc tuning and updates;

interpretation/interpret: prefixes within locale expression are mandatory by default;

locale_expression: mandatory as parameter; misc tuning and simplifications of parsers;

register_locale: produce stamps at the spot where elements are registered; tuned signature; misc internal tuning and simplification;

pretty_rule/print_results: no thm status here -- it is potentially slow and mostly uninformative/confusing as long as proofs are still unfinished;

pretty_thm_aux etc.: explicit show_status flag;

simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;

@{binding} is not a constructor term and should not be inlined, otherwise we loose value polymorphism;

tuned;

use more informative Thm.proof_body_of for oracle demo;

Proofterm.approximate_proof_body;

fulfill_proof/thm_proof: pass whole proof_body, not just the projection to proof (which might be incomplete); more explicit oracle_proof;

removed misleading make_proof_body, make_oracles, make_thms, which essentially assume a *full* proof; added approximate_proof_body -- replaces former make_proof_body; added all_oracles_of; oracle_proof: explicit oracle result; fulfill_proof/thm_proof: require proper proof_body futures, to maintain full account of oracles and thms (repairs a serious problem of the old version);

avoid mixing of left/right associative infixes, to make it work with experimental Poly/ML 5.3 branch;

simplified addPrettyPrinter setup: may pass (fn ...) directly if type constraints are omitted -- addPrettyPrinter treated as a special case internally;

status_of: need to include local promises as well!

status_of: simultaneous list;

display derivation status of thms;

recover old ids;

report ML typing;

merged

merged

NEWS: [arith]

get_index: produce index of next pending token, not the last one;

register token positions persistently with context; report some aspects of parse trees; removed obsolete CPPrintInAlphabeticalOrder; tuned;

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