use_text: added name argument;

Added simproc list_neq (prompted by an application)

Added lists-as-multisets functions

Simple and efficient binary numerals.

added HOL/ex/Binary.thy;

tuned ML setup;

* ML within Isar: antiquotations;

added @{theory};

added the_context_finished; eval_wrapper: Output.debug; simplified antiq signatures; added basic antiquotations; tuned;

Toplevel.debug: coincide with Output.debugging;

ML tactic: proper context for compile and runtime;

tuned;

added @{simpset};

added is_finished_thy;

Output.debug: non-strict; renamed Output.show_debug_msgs to Output.debugging (coincides with Toplevel.debug);

tuned ML setup; added @{claset};

added @{clasimpset};

added @{claset};

tuned;

tuned;

renamed Isar/isar_output.ML to Thy/thy_output.ML; tuned messages; Antiquote.scan_arguments (moved from here); moved ML context stuff to from Context to ML_Context;

moved ML context stuff to from Context to ML_Context; theorem(s): same kind;

results: proper context;

tuned Scan.extend_lexicon;

renamed IsarOutput to ThyOutput; tuned Scan.extend_lexicon; moved ML context stuff to from Context to ML_Context;

moved parts to spec_parse.ML; tuned signature -- more exports;

removed obsolete Method; added parse (from outer_parse.ML); moved ML context stuff to from Context to ML_Context; tactic: no need to rebind thm/thms;

renamed IsarOutput to ThyOutput; moved parts of OuterParse to SpecParse; renamed OuterParse locale_target to target;

added various ML setup functions (from sign.ML, pure_thy.ML);

removed obsolete Attribute;

tuned signature; added scan_arguments;

renamed Isar/isar_output.ML to Thy/thy_output.ML; renamed Isar/term_style.ML to Thy/term_style.ML; renamed Isar/thy_header.ML to Thy/thy_header.ML; added Isar/spec_parse.ML; added Thy/ml_context.ML; load outer_parse.ML early, moved later parts to spec_parse.ML; tuned order;

tuned signature of extend_lexicon;

moved ML translation interfaces to isar_cmd.ML;

moved thm/thms to ml_context.ML; moved generic_setup, add_oracle to isar_cmd.ML;

moved inst from drule.ML to old_goals.ML;

tuned order;

renamed Isar/term_style.ML to Thy/term_style.ML;

renamed Isar/thy_header.ML to Thy/thy_header.ML;

ML context and antiquotations (material from context.ML); added thm/thms (from pure_thy.ML); added support for ML antiquotations;

Parsers for complex specifications (material from outer_parse.ML);

renamed Isar/isar_output.ML to Thy/thy_output.ML; renamed Isar/term_style.ML to Thy/term_style.ML; renamed Isar/thy_header.ML to Thy/thy_header.ML; added Isar/spec_parse.ML; added Thy/ml_context.ML;

moved parts of OuterParse to SpecParse; renamed OuterParse locale_target to target;

moved parts of OuterParse to SpecParse;

HOL-Lambda: usedir -m no_brackets;

simplified ML setup;

tuned;

renamed IsarOutput to ThyOutput;

updated;

moved ML context stuff to from Context to ML_Context;

renamed IsarOutput to ThyOutput; moved ML context stuff to from Context to ML_Context;

interpreter for Finite_Set.finite added

reformatted to 80 chars/line

Theorem "(x::int) dvd 1 = ( ¦x¦ = 1)" added to default simpset. This solves the goals like "~ 4 dvd 1". This used to fail before.

adapted ML context operations;

added generic_theory_of; adapted ML context operations;

added 'declaration' command;

added 'declaration' command; adapted ML context operations;

adapted ML context operations;

ML context: full generic context, tuned signature;