updated

Refer to major premise of induction rule via "thm_style prem1".

Added named_thms antiquotation.

Replaced "hand-made" files by generated files in Inductive/document.

LaTeX code is now generated directly from theory files.

LaTeX code is now generated directly from Even and Advanced theories.

LaTeX code is now generated directly from theory file.

DEEPEN: Use priority message channel for interim messages (not warnings).

Direct priority and tracing channels properly.

tidying using metis

fileident --- produce file identification based;

added ISABELLE_FILE_IDENT (command line for source file identification);

adapted TextIO.inputLine;

tuned comment;

avoid redundant variables in patterns (which made Alice vomit);

Full sort information by default. Race condition on successful proofs fixed.

Added hypotheses.

Added clause for hypotheses to proof_of_xml function.

use /usr/proj/polyml/polyml-5.1-test, which might be more stable;

reverted fun->recdef, since there are problems with induction rule

Pure theory setup.

Generic print mode.

moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);

simplified loading of ML files -- no static forward references;

moved print_translations from Pure.thy to Syntax/syn_trans.ML;

added General/print_mode.ML, pure_setup.ML;

tuned specifications;

use function package

more proofs

some interface cleanup

added lemma binding: accpI = accp.accI

updated

tidied using sledgehammer

tidied

tidied using sledgehammer

tidied using sledgehammer

clarified structure names

added function for case certificates

dropped outer ROOT structure for generated code

tuned

fixed SML/NJ int problem

updated

tuned;

updated

updated;

tuned signature; misc cleanup / simplification;

sys_error;

simplified using Markup.get_int; renamed PgipParser to OldPgipParser;

added skeleton for print_mode setup; removed unused stuff;

tuned spacing;

renamed PgipParser to OldPgipParser;

Parsing theory sources without execution (via keyword classification).

exported command_keyword; tuned;

command 'declare': proper thy_decl;

added get_string, get_int; tuned;

added ProofGeneral/pgip_parser.ML;

tuned error faces;

tries to solve goal via TrueI

tuned markup;

replaced OuterLex.name_of by more sophisticated OuterLex.text_of;

Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols); replaced OuterLex.name_of by more sophisticated OuterLex.text_of; tuned;

Buffer.markup;

removed ident, space; added antiq; tuned;

added markup operation;

Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);

Added entry for new inductive definition package.

Proof terms for meta-conjunctions are now normalized before splitting up the conjunctions.

Added function norm_proof for normalizing the proof term corresponding to a theorem.

Added function rew_proof (for pre-normalizing proofs).

Function unify_consts moved from OldInductivePackage to PrimrecPackage.

Adapted to new inductive definition package.

Renamed accessible part for predicates to accp.

renamed inductive2 to inductive.

Renamed inductive2 to inductive.

Hide member constant.

Reverted renaming of "member".

changed sources for HOL-Complex-Matrix

Restored set notation in Multiset theory.

added dummy makestring function

Renamed inductive2 to inductive.

fixed for SML/NJ

Adapted to new inductive definition package.

Adapted to changes in Accessible_Part theory.

Function unify_consts moved from OldInductivePackage to PrimrecPackage.

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;