improved LocalDefs.add_def;

mk_partial_rules_mutual: expand result terms/thms;

removed with_local_path -- LocalTheory.note admits qualified names; TheoryTarget.init;

moved the_single to Pure/library.ML; tuned;

TheoryTarget.init;

tuned comments;

tuned method syntax: polymorhic term argument; tuned rule instantiation;

tuned;

Fixed the printing of the used theorems by maintaining separate lists for each subgoal. Retains the ATP input files if debugging is on.

Tidied code to delete tmp files. Fixed the printing of the used theorems by maintaining separate lists for each subgoal.

renamed the combinator laws

Improved detection of identical clauses, also in the conjecture

Refinements to abstraction. Seeding with combinators K, I and B.

examples for hex and bin numerals

Changed and removed some functions related to combinators, since they are Isabelle constants now.

Now the DFG output includes correct declarations of c_fequal, but not hEXTENT

improvements to abstraction, ensuring more re-use of abstraction functions moving some functions to Pure/drule.ML

facts about combinators

a few new functions on thms and cterms

reorganize and speed up termdiffs proofs

fixed bug in linear arith

improvements for Haskell serialization

insert replacing ins ins_int ins_string

cleaned up some mess

clarified header comments

insert replacing ins ins_int ins_string

*** empty log message ***

tuned

Improved error reporting

nnf_simpset built statically