New wrapper for defining inductive sets with new inductive predicate package.

Old (co)inductive command is now replaced by (co)inductive_set.

Reorganization due to introduction of inductive_set wrapper.

Improved code generator for Collect.

Renamed inductive2 to inductive.

Fix nested PGIP messages. Update for schema simplifications.

Moved unify_consts to PrimrecPackage.

- Renamed inductive2 to inductive - Renamed some theorems about transitive closure for predicates

Adapted to changes in Predicate theory.

Adapted to new inductive definition package.

Renamed accessible part for predicates to accp.

Track schema changes: merge messagecategory with area attributes

bot is now a constant.

Restored set notation.

- Renamed inductive2 to inductive - Renamed some theorems about transitive closure for predicates

Track schema changes: remove cleardisplay, proofstate messages. Simplify attributes on cleardisplay, normalresponse.

Track schema changes: add area attribute to pgml packet. Also add quoted Raw element [hack for Isabelle bottom-up XML production]

Renamed inductive2 to inductive.

Adapted to new inductive definition package.

New operations on tuples with specific arities.

Adapted to changes in infrastructure for converting between sets and predicates.

rtrancl and trancl are now defined using inductive_set.

Removed wf_implies_wfP and wfP_implies_wf from list of hints again.

- Moved infrastructure for converting between sets and predicates to Tools/inductive_set_package.ML - Adapted conversion rules to new format (now use standard op : and Collect operators rather than Collect2 and member(2)) - Removed bounded quantifiers for predicates

Adapted to new package for inductive sets.

Inserted definition of in_rel again (since member2 was removed).

Added ML bindings for sup_fun_eq and sup_bool_eq.

top and bot are now constants.

Renamed inductive2 to inductive.

acc is now defined using inductive_set.

Added new package for inductive sets.

Adapted to new inductive definition package.

Adapted to changes in inductive definition package.

tuned comment markup;

treat OuterLex.Error;

separated Malformed (symbolic char) from Error (bad input); unparse: Output.escape_malformed; name_of: use unparse;

Output.escape_malformed;

added escape_malformed (failsafe);

Basic editing of theory sources.

tuned;

export html_mode, begin_document, end_document;

renamed XML.Rawtext to XML.Output;

export get_lexicons;

added kind_of; unparse: extra care for Malformed;

Markup.enclose;

more markup for inner and outer syntax; added enclose;

simplified funpow, untabify;

added Thy/thy_edit.ML;

added some markup for outer syntax;

clarified merge of module names

now a monolithic module

now works with SML/NJ

tuned

improvement for code names

removed proof dependency on transitivity theorems

moved lfp_induct2 here

clarified import

moved lfp_induct2 to Relation.thy

moved some finite lemmas here

moved finite lemmas to Finite_Set.thy

added print_mode setup (from pretty.ML); removed no_state;

Markup.add_mode;

removed no_state markup -- produce empty state; Markup.add_mode;

Markup.output; removed no_state markup -- produce empty state;

moved source cascading from scan.ML to source.ML;

infixr || (more efficient); tuned signature; removed unused trace'; moved source cascading from scan.ML to source.ML; tuned;

moved print_mode setup for markup to markup.ML;

Markup.output;

use position.ML earlier;

Add widthN to signature

cd ISABELLE_HOME/etc;

adjusted

updated keywords

simplified, tuned

re-expanded paths

replaced code generator framework for reflected cooper

expanded fragile proof

extended - convers now basic lcm properties also

constant dvd now in class target

moved lemma zdvd_period here

introduced (auxiliary) class dvd_mod for more convenient code generation

tuned;

nested source: explicit interactive flag for recover avoids duplicate errors;

tuned dead code;

use Position.file_of; removed strange comments;

toplevel_source: interactive flag indicates intermittent error_msg; nested source: error msg passed to recover; tuned source positions;

Malformed token: error msg; scan: explicit handling of malformed symbols from previous stage; source: interactive flag indicates intermittent error_msg; tuned;

adapted OuterLex/T.source;

scan: changed treatment of malformed symbols, passed to next stage; tuned sym_explode;

nested source: error msg passed to recover;

tuned signature; nested source: error msg passed to recover;

replaced name by file (unquoted); str_of: markup; misc cleanup;

moved Path.position to Position.path;

proper position markup; added properties operation; tuned;

use position.ML after pretty.ML;

removed target RAW-ProofGeneral (impractical to maintain);

declare: disallow quote (") in names;

removed legacy ML file; fixed prems_conv;

HOL-Complex-Matrix: fixed deps -- sort of;

adopted to new computing oracle and fixed bugs introduced by tuning

added computing oracle support for HOL and numerals

new version of computing oracle

simplified writeln_fn;

prompt: plain string, not output;

type output = string indicates raw system output;

symbolic output: avoid empty blocks, 1 space for fbreak;

tuned;

thm tag: Markup.property list;

gensym: slightly more obscure prefix descreases probability of name clash;

replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;

attribute tagged: single argument;

updated;

simplified Symtab;

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;