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;

added remove_trrules(_i); tuned;

added is_elim (from Provers/classical.ML);

added 'no_translations';

added pretty_stmt; tuned;

declared_const: check for type constraint only, i.e. admit abbreviations as well; added del_trrules(_i);

ObjectLogic.is_elim;

tuned constdecl; added 'no_translations';

updated;

Pure: no_translations;

refined representation of instance dictionaries

entry for Library/AssocList

First version of function for defining graph of iteration combinator.

got rid of type Sign.sg;

renamed plus to add;

renamed const minus to subtract;

simplified AxClass interfaces;

added axclass_instance_XXX (from axclass.ML); Sign.read/cert_arity;

*** empty log message ***

added read_class, read/cert_classrel/arity (from axclass.ML);

moved read_class, read/cert_classrel/arity to sign.ML; axclass: moved outer syntax to isar_syn.ML; instance: moved to Tools/class_package.ML; simplified interfaces; tuned;

use axclass.ML earlier (in Isar/ROOT.ML);

nbe: no_document;

tuned;

exporting reapAll and killChild

text delimiter fixed

comment delimiter fixed

clauses now use (meta-)hyps instead of (meta-)implications; significant speedup

fix for document preparation

Added Library/AssocList.thy

renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.

Changed some warnings to debug messages

Frequency analysis of constants (with types). Ability to restrict the number of accepted clauses.

Shortened the exception messages from assume.

METAHYPS catches THM assume exception and prints out the terms containing schematic vars.

added many simple lemmas

Added more functions to the signature and tidied up some functions.

tuned;

tuned some proofs

select_goals: split original conjunctions;

method: goal restriction defaults to [1];

infer_derivs: avoid allocating empty MinProof;

tuned;

Isar/method: goal restriction;

constdecl: always allow 'where';

deleted some proofs "on comment"

tuned some proofs

tuned some of the proofs about fresh_fun

first running version of type classes

first running version of type classes

first running version of type classes

Frequency strategy. Revised indentation, etc.

*** empty log message ***

added ROOT.ML

Indentation

Tidying and restructuring.

Tidying and tracing. Handling exn CLAUSE so that errors don't reach top-level.

Tidying. clausify_rules_pairs_abs now returns clauses in the same order as before. Removal of the unused err_list.

Tidying. New invoke_atp_ml for top-level debugging. Flag to force FOL mode.

Tidying, and getting rid of SELECT_GOAL (as it does something different now)

Added HOL-ZF to Isabelle.

substantial improvement in codegen iml

Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset. The hash table (for removing duplicate) now stores clauses as Term.term with names.

relevance_filter takes input axioms as Term.term.

Proof reconstruction now only takes names of theorems as input.

Added tptp_write_file to write all necessary ATP input clauses to one file.

tptp_write_file now takes goals and axioms as Term.term and writes them to a file.

Added functions to retrieve local and global atpset rules. cnf thms to Term.term format.

Moved the settings for ATP time limit to res_atp.ML

Merged res_atp_setup.ML into res_atp.ML. HOL translation is integrated with background Isabelle-ATP linkup. Both ATP methods and background linkup retrieve lemmas stored in claset, simpset and atpset.

When ATP methods call ATPs, all input clauses from one subgoal are written to one file.

Merged res_atp_setup.ML into res_atp.ML.

SELECT_GOAL: fixed trivial case;

fixed a typo in a comment

tuned;

method: SelectGoals;

method: syntax for SelectGoals;

text: added SelectGoals;

tuned conj_curry;

added extract, retrofit;

added mk_conjunction; tuned conj_curry;

method: restriction to first n sub-goals;

minor changes

more examples

changed and retracted change of location of code lemmas.

ignore repeated vars on lhs, cleanup

improvements for nbe

reformatting

subset_refl now included using the atp attribute