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;

updated

Fix pgmlsymbolsoff

tuned a bit the proofs

correctled left/right following of another context in zipto.

induction rules for trancl/rtrancl expressed using subsets

Deleted mk_fol_type, since the constructors can be used directly

Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC minimize_applies is now by default TRUE!

fixed typo introduced by me

changed dictionary representation to explicit classrel witnesses

reverted order of classrels

cleanup

formalisation of Crary's chapter on logical relations (in the book on Advanced Topics in Type Systems) done by Narboux and Urban

added capabilities to handle mutual inductions

refined and added example for ExecutableRat

introduced binding concept

slight cleanup

renamed locale partial_order to order

refined and added example for ExecutableRat

updated keywords

added sections on mutual induction and patterns

optimized translation of HO problems

Reverted to structure representation with records.

more term inspection

introduced binding concept

adjusted manual

well-founded relations for the integers