proper collapse_let

new code generator framework

dropped Library.lcm

tuned

code generation for dvd

simplified keyword setup

GPL -> BSD

*** empty log message ***

updated for metis method

recoded

simplified

completed some references

changes for type class ring_no_zero_divisors

*** empty log message ***

added NBE

removed removed lemmas

fixed undo: try undos_proof first!

tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW; eta_long_tac; tuned;

removed theorem

removed redundant lemma

removed redundant lemmas

commented changes in HOL/Ring_and_Field.thy, and in HOL/Real/RealPow.thy

removed "sum_tools.ML" in favour of BalancedTree

added eta_long_conversion;

added eta_long_tac;

added reasonably efficient add_cterm_frees;

made type conv pervasive; removed obsolete eta_conv (cf. Thm.eta_long_conv);

made type conv pervasive; Thm.eta_long_conversion; Thm.add_cterm_frees; tuned;

Thm.eta_long_conversion;

made type conv pervasive; Thm.add_cterm_frees;

Thm.add_cterm_frees;

made type conv pervasive;

made type conv pervasive; tuned;

tex problem fixed

tuned and used field_simps

*** empty log message ***

*** empty log message ***

new lemmas

*** empty log message ***

tuned and renamed group_eq_simps and ring_eq_simps

fix looping simp rule

reinstate real_root_less_iff [simp]

merge is now identity

new method "elim_to_cases" provides ad-hoc conversion of obtain-style elimination goals to a disjunction of existentials.

section headings

add thm antiquotations

spelling

add thm antiquotations

changed simp rules for of_nat

tuned proofs -- avoid implicit prems;

moved quantifier elimination tools to Tools/Qelim/;

moved Presburger setup back to Presburger.thy;

tuned proofs -- avoid implicit prems;

tuned proofs -- avoid implicit prems;

renamed NatSimprocs.thy to Arith_Tools.thy; incorporated HOL/Presburger.thy into NatSimprocs.thy;

tuned;

adapted tool setup;

added Ferrante-Rackoff setup;

tuned comments;

moved HOL/Tools/Presburger/qelim.ML to HOL/Tools/qelim.ML;

Ferrante-Rackoff quantifier elimination.

Context data for Ferrante-Rackoff quantifier elimination.

replaced Real/Ferrante-Rackoff tool by generic version in Main HOL;

Dense linear order witout endpoints and a quantifier elimination procedure in Ferrante and Rackoff style.

renamed metis-env.ML to metis_env.ML;

added Id;

fine tune automatic generation of inversion lemmas

integration of Metis prover

renamed metis-env to metis-env.ML;

tuned comments;

obsolete (cf. ATP_Linkup.thy);

added Tools/metis_tools.ML;

added Metis setup (from Metis.thy);

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);