renamed ML_exc to ML_exn;

Show the use of reflection attribute; fixed comments about the order of absorbing equations : f (C x) = x ; now automaically tried as last;

Changed syntax for the reflection method (reify unchanged). reflection takes an optional set of theorems for reification then several correctness theorems are specified by rules:'' then the optional term is specified by only:

Try several correctness theorems for reflection; rearrange cong rules to avoid the absoption cases;

Context data now consist of eqations for reification and equations for correctness theorems for reflection; Added attribute reflection to store correctness theorems to be trued by default

simplified/more robust print_state; more robust prompt markup;

export mode_markup; added symbolic output (via print_mode); misc cleanup;

added markup for pretty printing;

Corrected erronus use of compiletime context to the runtime context

make smlnj happy;

toplevel prompt/print_state: proper markup, removed hooks;

toplevel prompt/print_state: proper markup, removed hooks; tuned;

pretty_state: subgoal markup; tuned;

added markup_chunks;

added toplevel markup; misc cleanup;

use markup.ML earlier;

removed obsolete disable_pr/enable_pr; added old print_goals from display.ML;

pretty_goals_aux: subgoal markup; print_goals etc.: moved old version to old_goals.ML, removed hooks; tuned;

pr_goals: adapted Display.pretty_goals_aux; pr_goals/prterm: proper context; tuned;

export attribute;

pretty_sort/typ/term: markup;

pretty: markup for syntax/name of authentic consts; datatype symb: String (potential markup) vs. Space (no markup);

depend on alist.ML, markup.ML;

markup: emit as control information -- no indent text;

added property conversions; tuned;

position: line and name; tuned operations;

moved markup.ML before position.ML;

The order for parameter for interpretation is now inversted: f t env0 env1 ... envn = ... where t is the type to be reified;

Common markup elements.

simplified pretty token metric: type int; added command markup; token translations: proper treatment of skolems; separate print_mode setup for Output/Pretty;

simplified pretty token metric: type int; separate print_mode setup for Output/Pretty;

moved General/xml.ML to Tools/xml.ML; actually use pgml.ML;

tuned;

simplified output mode setup; removed unused symbol_output; tuned;

added print_mode setup: indent and markup; simplified pretty token metric: type int; added general markup for blocks; removed unused writelns;

renamed raw to escape; simplified pretty token metric: type int; simplified print_mode setup: output_width and escape; moved pretty setup to pretty.ML;

simplified pretty token metric: type int;

moved General/xml.ML to Tools/xml.ML;

added General/markup.ML; moved General/xml.ML to Tools/xml.ML;

added class skolem, command;

more interpretations

Produce good PGML 2.0

cosmetic (line length fixed)

Some examples for reifying type variables

Tuned document

Cleaned add and del attributes

Reification now deals with type variables

Cumulative reports for Poly/ML profiling output.

Update PGML version, add system name

tuned interfaces: atomize, atomize_prems, atomize_prems_tac; removed atomize_cterm/goal;

added type conv; merge_thys: removed dead exception handlers; tuned;

removed comments -- no exception TERM; merge_list: exception THEORY;

added is_reflexive;

tuned;

simplified has_meta_prems;

moved type conv to thm.ML; renamed Conv.is_refl to Thm.is_reflexive; misc tuning of basic conversions;

the_theory/proof: error instead of exception Fail;

renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac; added flat_rule filter for addXXs etc.;

renamed Conv.is_refl to Thm.is_reflexive;

renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac; simplified ObjectLogic.atomize;

simplified ObjectLogic.atomize;

renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;

Revert body of pgml to match schema for now [change bad for Broker]

Classify -- comments as ordinary comments (no undo)

tuned;

avoid polymorphic equality; added dest_judgment;

sort_le: tuned eq case;

tuned goal conversion interfaces;

else_conv: only handle THM | CTERM | TERM | TYPE; prems_conv: no index; renamed goal_conv_rule to gconv_rule;

avoid polymorphic equality; Numeral.mk_cnumber;

tuned;

moved mk_cnumeral/mk_cnumber to Tools/numeral.ML; tuned;

avoid polymorphic equality; do not export ring_conv (which is not a conversion anyway); renamed algebra_tac to ring_tac; ring_tac: simplified tactic wrapper, no longer handles ERROR;

avoid polymorphic equality; removed dead code;

avoid polymorphic equality;

removed dest_cTrueprop (cf. ObjectLogic.dest_judgment);

Logical operations on numerals (see also HOL/hologic.ML).

added Tools/numeral.ML;

common normalizer_funs, avoid cterm_of;

Numeral.mk_cnumber;

PGML abstraction, draft version

Use pgml

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;

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