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;

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.