added HOL-Nominal-Examples;

The Metis prover (slightly modified version from Larry);

avoid using implicit prems in assumption

Added flexflex_first_order and tidied first_order_resolution

A more robust flexflex_unique

remove simp attribute from of_nat_diff, for backward compatibility with zdiff_int

tuned error msg

Remove dedicated flag setting elements in favour of setproverflag.

Remove dedicated flag setting elements in favour of setproverflag. Restore displayconfig response in askpgip.

Synchronize schema with current version

added lemmas

added meta_impE

change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems

section headings

simplify some proofs

oops -- fixed profiling;

Balanced binary trees (material from library.ML);

profiling: observe no_timing;

added raw_tactic;

moved balanced tree operations to General/balanced_tree.ML;

added with_subgoal;

balanced conjunctions; tuned interfaces; tuned;

balanced conjunctions; added split_defined (from conjunction.ML);

added General/balanced_tree.ML;

BalancedTree;

balanced conjunctions;

tuned;

generalized proofs so that call graphs can have any node type.

macbroy5: trying -j 2;

tuned conjunction tactics: slightly smaller proof terms;

tuned laws for cancellation in divisions for fields.

moved nonzero_mult_divide_cancel_right to Ring_and_Field as nonzero_mult_divide_cancel_right'; tuned proofs

Added eta_conv and eta-expansion conversion: waiting for it to be in thm.ML; exported is_refl

gen_qelim_conv now reduces the universal quatifier to the existential one; Now also deals with Ex f for eta-contracted f;

thin_prems_tac first max-scopes universal quantifiers; eta_conv moved to Pure/conv.ML

Tuned error messages; tuned;

normalizer conversions depend on the proof context; added functions for conversion and wrapper that sill depend on the variable ordering (_ord)

added theorems nonzero_mult_divide_cancel_right' nonzero_mult_divide_cancel_left' ordered_field_no_lb ordered_field_no_ub

moved lemma all_not_ex to HOL.thy ; tuned proofs

Tuned instantiation of Groebner bases to fields

added Theorem all_not_ex

renamed vars in zle_trans for compatibility

tuned

The simprocs "divide_cancel_factor" and "ring_eq_cancel_factor" no longer need class numeral_ring. This made a number of special simp-thms redundant.

Locally added definition of "int :: nat => int" again to make code generation work.

made divide_self a simp rule

Removed thunk from Fun

Church numerals added

method assumption: uniform treatment of prems as legacy feature;

tuned proofs;

tuned proofs: avoid implicit prems;

fixed term_constants (impact on is_relevant); terms in generalize_tac are sorted before we abstract over them (to *try* to avoid the case when a term to be abstracted over already occurs in an other)

no computation rules in the pre-simplifiaction set

Added some lemmas to default presburger simpset; tuned proofs

tuned proofs: avoid implicit prems;

tuned proofs: avoid implicit prems; tuned partition proofs;

Now ResHolClause also does first-order problems!

Now also handles FO problems

Deleted unused code

tidied

tuned proofs: avoid implicit prems;

clarified who we consider to be a contributor

Fixed Problem with ML-bindings for thm names;

fixed filter syntax