fixed argument order in calls to Integer.pow

added binop_cong_rule;

export dlo_conv; removed redundant auxiliary operations; tuned exceptions -- avoid error here; simplified tactic wrapper (CSUBGOAL, CONVERSION); merge_ss: recover simpset context; tuned;

replaced HOLogic.Trueprop_conv by ObjectLogic.judgment_conv;

*** empty log message ***

*** empty log message ***

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;