moved theory presentation to Isar/ROOT.ML;

hide consts in Numeral.thy;

tuned syntax/abbreviations;

unfold(ed): not necessrily meta equations;

Made "empty" an abbreviation.

*** empty log message ***

Removed old set interval syntax.

pretty_term: late externing of consts (support authentic syntax);

pretty: late externing of consts (support authentic syntax);

removed fix_mixfix; added const_mixfix, mixfix_const;

abbreviation(_i): do not expand abbreviations, do not use derived_def;

add_abbrevs(_i): support print mode; pretty_term': expand abbreviations only for well-typed terms; added expand_abbrevs; tuned;

abbrevs: support print mode;

simplified handling of authentic syntax (cf. early externing in consts.ML); simplified extern_term;

'abbreviation': optional print mode;

tuned;

pretty_term': early vs. late externing (support authentic syntax); add_abbrevs(_i): support print mode and authentic syntax;

print_theory: print abbreviations nicely;

added intern/extern/extern_early; added expand_abbrevs flag; strip_abss: demand ocurrences of bounds in body; const decl: added flag for early externing (disabled for authentic syntax); abbrevs: support print mode; major cleanup;

refined 'abbreviation';

made symlink relative

made symlink relative

converted Müller to Mueller to make smlnj 110.58 work

Fixed bug that caused proof of induction rule to fail for inductive sets with trivial introduction rules such as "x : S ==> x : S".

remame ASeries to Arithmetic_Series

Added alternative version of thms_of_proof that does not recursively descend into proofs of (named) theorems.

hash table now stores thm and get_clasimp_atp_lemmas returns thm rather than term.

filter now accepts axioms as thm, instead of term.

tptp_write_file accepts axioms as thm.

added another function for CNF.

lemmas returned from ResClasimp.get_clasimp_atp_lemmas are thm rather than term.

renamed ASeries to Arithmetic_Series, removed the ^M

modified the perm_compose rule such that it is applied as simplification rule (as simproc) in the restricted case where the first permutation is a swapping coming from a supports problem also deleted the perm_compose' rule from the set of rules that are automatically tried

cleanup in typedef/datatype package

added explicit serialization for int equality

adapted for definitional code generation

cleanup in datatype package

small type annotation fix

added hook for codegen_theorems.ML

adaptions to change in typedef_package.ML

added functions for definitional code generation

added definitional code generator module: codegen_theorems.ML

minor changes

exported specification names

minor extensions

pool of constants; definition expansion; current best settings

removed some illegal characters: they were crashing SML/NJ

Removal of unused code

Simplified version of Jia's filter. Now all constants are pooled, rather than relevance being compared against separate clauses. Rejects are no longer noted, and units cannot be added at the end.

renamed map_val to map_ran

added map_val, superseding map_at and substitute ----------------------------------------------------------------------

some internal cleanup

removed illegal character codes

simplified the proof at_fin_set_supp

changed abbreviation for "infinite" back to translation because something didn't work during (output).

lazy patterns in lambda abstractions

changed the it_prm proof to work for recursion

tuned some proofs

Removed occurrences of makestring, which does not exist in SML/NJ.

Converted translations to abbbreviations. Removed a few odd functions from Map and AssocList. Moved chg_map from Map to Bali/Basis.

Replaced iteration combinator by recursion combinator.

detection of definitions of relevant constants

Only display atpset theorems if Output.show_debug_msgs is true.

added the first two simple proofs of the recursion combinator

comment fixed

Introduction of "whitelist": theorems forced past the relevance filter

Slight simplification of proofs

Removal of obsolete strategies. Initial support for locales: Frees and Consts treated similarly.

comment for conjI added

translations -> abbreviations (a cool feature)

fixed example;

mark_boundT: produce well-typed term;

subtract (op =); pretty_proof: no abbrevs;

avoid polymorphic equality; tuned;

avoid polymorphic equality; subtract (op =);

moved gen_eq_set to library.ML;

added ~$$ (negative literal); combinators: avoid code duplication; tuned extend_lexicon;

avoid polymorphic equality;

remove (op =); tuned;

gen_eq_set, remove (op =);

abbreviation upto, length;

added subtract; tuned;

subtract (op =);

remove (op =);

Now SML/NJ-friendly (IntInf)

Removal of unnecessary simprules: simproc cancel_numerals now works without add_Suc, while the reason for the horrible isolateSuc is not known.

interpret: Proof.assert_forward_or_chain;

subsetI is often necessary

Now the setup for cancel_numerals accepts mixed Sucs/+ where the Sucs no longer need to be outermost.

Tuned signature of Locale.add_locale(_i).

simplified mg_domain (use Sign.classes/arities_of); removed unused lift_local_theory_yield;

made $$ and "this" monomorphic (string);

tuned;

export arities_of instead of classes_arities_of;

updated;

renamed const less to lt;

renamed constant less in lattice

fixed problem with proof reconstruction by adding add_Suc to arith-simpset.

added parser locale_expr_unless

fixed clsvar bug

add_locale(_i) returns internal locale name.

added example for operational classes and code generator

slight improvement in serializer, stub for code generator theorems added

Renamed setsum_mult to setsum_right_distrib.

Internal restructuring: local parameters.

renamed op < <= to Orderings.less(_eq)

New interface function parameters_of_expr.

add_inst_arity_i renamed to prove_arity.

rename_frees: treat trivial names; monomorphic: tuned invented names;

added singleton;

updated;

turned string_of_mixfix into pretty_mixfix;

added monomorphic; export hidden_polymorphism;

added 'print_statement' command;

added print_stmts;

added pretty_statement;

added command, keyword; added chunks2;

Output.add_mode: keyword component;

string_of_mixfix;

print_statement;