simplified a proof

tuned;

CONVERSION: handle TYPE | TERM | CTERM | THM;

proper use of ioa_package.ML;

tuned;

tuned is_comb/is_binop -- avoid construction of cterms; removed conjunction rules (cf. HOLogic.conj_XXX);

HOLogic.conj_intr/elims; removed obsolete assocd/assoc; removed dead string_of_pol; tuned;

use mucke_oracle.ML only once;

assume basic HOL context for compilation (antiquotations); added dest_cTrueprop; tuned Trueprop_conv; added low-level conj_intr/elim/elis (dire need for @{rule} antiquotation!);

proper use of function_package ML files;

use hologic.ML in basic HOL context; tuned proofs;

to handle non-atomic assumptions

rename class dom to ring_1_no_zero_divisors (cf. HOL/Ring_and_Field.thy 1.84 by huffman);

convert instance proofs to Isar style

Dependency on reflection_data.ML to build HOL-ex

Generalized case for atoms. Selection of environment lists is allowed more than once.

More examples

reflection and reification methods now manage Context data

Context Data for the reflection and reification methods

rename class dom to ring_1_no_zero_divisors

rewrite_goal_tac;

replaced Conv.goals_conv by Conv.prems_conv;

exported meta_rewrite_conv; CONVERSION tactical;

CONVERSION tactical; MetaSimplifier.rewrite_goal_tac;

removed obsolete eta_long_tac;

added CONVERSION tactical; tuned signature;

tuned rotate_prems; tuned comments;

moved (asm_)rewrite_goal_tac from goal.ML to meta_simplifier.ML (no longer depends on SELECT_GOAL);

removed obsolete mk_conjunction_list, intr/elim_list;

removed obsolete goals_conv (cf. prems_conv); added efficient goal_conv_rule; tuned comments;

Conjunction.intr/elim_balanced; CONVERSION tactical; tuned;

CONVERSION tactical; Simplifier.rewrite_goal_tac;

Conjunction.mk_conjunction_balanced;

CONVERSION tactical;

Fixed problem with patterns in lambdas

fixed an issue with mutual recursion

instance pordered_comm_ring < pordered_ring

Added pattern maatching for lambda abstraction

revised the discussion of type classes

Generic QE need no Context anymore

Handle exception TYPE

Tuned proofs

added ordered_ring and ordered_semiring

tuned arithmetic modules

bug fixes to proof reconstruction

dropped local cg cmd

dropped toplevel lcm, gcd

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

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

updated 'find_theorems' -- moved ProofGeneral specifics to ProofGeneral/CHANGES;

tuned proofs: avoid implicit prems;

int abbreviates of_nat

tuned proofs: avoid implicit prems; tuned;

tuned proofs: avoid implicit prems; major cleanup of proofs/document;

tuned comments;

tuned proofs: avoid implicit prems;

clean up instance proofs; reorganize section headings

reactivated theory Class;

added the Q_Unit rule (was missing) and adjusted the proof accordingly

* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account; * Isar: implicit use of prems from the Isar proof context is considered a legacy feature;

generate_fresh works even if there is no free variable in the goal

tuned;

tuned proofs: avoid implicit prems;

removed constant int :: nat => int; int is now an abbreviation for of_nat :: nat => int

thm antiquotations

transaction: context_position (non-destructive only);

added map_current; simplified internal type proof;

tuned msg;

apply_method/end_proof: pass position; Method.Basic: include position;

renamed map to map_current;

tuned;

removed unused is_atomic;

renamed prove_raw to prove_internal; tuned;

merge/merge_refs: plain error instead of exception TERM;

Context positions.

added context_position.ML;

renamed Goal.prove_raw to Goal.prove_internal;

Method.Basic: include position;

tuned proofs: avoid implicit prems;

Basic text: include position; assumption/close: refer to non-atomic assumptions as well, implicit use of prems now considered legacy feature;

thm antiquotations

add lemma inj_of_nat

thm antiquotations

Unfortunately needed patch due to incompatibility with SML -- oo is infix and hence can not appear on the left handside of patterns

changed int stuff into integer for SMLNJ compatibility

more of_rat lemmas

add function of_rat and related lemmas

turned curry (op opr) into curry op opr --- because of smlnj

De-overloaded operations for int and real.

SML basis with type int representing proper integers, not machine words.

Tuned proofs : now use 'algebra ad: ...'

cooper_tac takes now two lists of theorems to be added/deleted from the simpset dor pre-simplification

changed val restriction to local due to smlnj

Changed normalizer Data to contain a simpset besides the list of instances; Before the method starts, it simplifies with this simpset; Added attribute 'algebra' to add and delete theorems from the simpset above;

Added algebra_tac; tuned;

Method now takes theorems to be added or deleted from a simpset for simplificatio before the core method starts

algebra_tac moved to file Tools/Groebner_Basis/groebner.ML; Method now takes theorems to be added or deleted from a simpset for simplificatio *before* the core method starts

nex example

Conversion for computation on constants now depends on the context

tuned setup for the fields instantiation for Groebner Bases;

Added dependency on file Groebner_Basis.thy

Added instantiation of algebra method to fields

hid constant "dom"

Removed from CVS, since obselete in the new Presburger Method;

Generated reflected QE procedure for Presburger Arithmetic-- Cooper's Algorithm -- see HOL/ex/Reflected_Presburger.thy