eliminated old Sign.read_term/Thm.read_cterm etc.;

moved ProofContext.pretty_proof to ProofSyntax.pretty_proof; read_term: imitate old behaviour (allow_dummies, mode_schematic);

export transfer_syntax; added allow_dummies feature (for legacy emulations); moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;

moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;

removed obsolete term reading operations (cf. old_goals.ML for legacy emulations);

added emulations for simple_read_term/read_term/read_prop (formerly in sign.ML);

removed obsolete read_def_cterms/read_cterm;

load proof term operations later;

more antiquotations;

OldGoals.read_prop;

OldGoals.simple_read_term;

simplified Abel_Cancel setup;

updated generated file;

pervasive cut_inst_tac;

added a progress lemma and tuned some comments

* Rules and tactics that read instantiations now demand a proper context;

added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML); pervasive operations; tuned;

renamed rename_params_tac to rename_tac;

removed obsolete global instantiation tactics (cf. Isar/rule_insts.ML); removed obsolete rename_tac, rename_last_tac; renamed rename_params_tac to rename_tac;

removed obsolete no_qed, quick_and_dirty_prove_goalw_cterm; removed obsolete abbreviations for ML tactic scripts;

removed obsolete global read_insts/read_instantiate (cf. Isar/rule_insts.ML);

inst1_tac: proper context;

pervasive RuleInsts;

updated generated file;

converted ML proofs;

added read_instantiate;

ML tactic: do not abstract over context again;

export eof;

removed obsolete inst;

atomize: proper context; RuleInsts.read_instantiate;

atomize: proper context;

RuleInsts.read_instantiate;

ptac/prolog_tac: proper context;

allE_Nil: only one copy, proven in regular theory source;

deriv_tac/DERIV_tac: proper context;

sum3_instantiate: proper context;

eliminated OldGoals.inst;

updated generated file;

method "tactic": only "facts" as bound value; added method "raw_tactic";

Export a wrapper for all semiring_normalizers

proper context for tactics derived from res_inst_tac;

added ~: and ~=; fixed SOME, which is now \<some> not \<epsilon>;

export subgoal_tac, subgoals_tac, thin_tac;

prove: full Variable.declare_term, including constraints;

prove_standard: more precises argument passing; proper context for tactics derived from res_inst_tac;

InductTacs.case_tac: removed obsolete declare, which is now part of Goal.prove;

simplified InductTacs.case_tac/induct_tac;

tuned proof;

removed obsolete nat_induct_tac -- cannot work without;

removed obsolete case_split_tac -- cannot work without;

removed unused excluded_middle_tac; proper context for tactics derived from res_inst_tac; tuned setup;

updated geenrated file;

qualified old res_inst_tac variants;

proper context for tactics derived from res_inst_tac;

updated generated file;

obsolete;

certify_term: reject qualified frees;

removed experimental Poplog/PML support; removed obsolete ML_SUFFIX; some reformatting;

removed obsolete ML_SUFFIX; some reformatting;

removed experimental Poplog/PML support;

removed obsolete ML_SUFFIX;

removed exotic 'token_translation' command;

proper name for LinearQuantifierElim;

removed old theorem database;

map_const: soft version, no failure here (recovers hiding of consts, because a hidden name is illegal and rejected later);

hide: delete all accesses from extra names -- reduces ambiguity in extern;

map_const: soft version, no failure here;

skolem_fact/thm: uniform numbering, even for singleton list; declare_skofuns: eliminated recovery via Clausify_failure -- should be sufficiently robust as is;

hide (open);

no_notation instead of hide;

* Recovered hiding of consts;

updated generated file;

back to CodeTarget.code_width;

hide -> hide (open)

use regular error function;

add lemma finite_image_approx; remove unnecessary sort annotations

change orientation of fix_eqI and convert to rule_format; add lemma fix_ind2

export just one setup function; more antiquotations; to_nnf: import open, avoiding internal variables (bounds); ThmCache: added table of seen fact names; reorganized skolem_thm/skolem_fact/saturate_skolem_cache: maintain seen fact names, ensure idempotent operation for Theory.at_end; removed obsolete skolem attribute (NB: official fact name unavailable here);

removed obsolete skolem declarations -- done by Theory.at_end;

tuned setup;

remove unnecessary import of Ffun; add lemma admD2

imports Ffun

ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context; eliminated obscure theory merge/transfer -- use explicit theory context instead;

ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;

sane versions of (qualified_)thms_of_thy;

Facts.dest/export_static: content difference; tuned;

dest/export_static: content difference; tuned comments;

declare_skofuns/skolem: canonical argument order; minor tuning;

Facts.dest/export_static: content difference;

correction

tuned

Removed hide swap

fixed type

lemma modified

typo

had to add rule: because induct_tac no longer works correctly

Hid swap

some reformatting;

added CK_Machine to the nominal section

soundness and completeness proofs for a CK machine as well as proofs for type preservation

emoved the parts that deal with the CK machine to a new theory

tuned header and comments

OldGoals.inst;

Drule.read_instantiate; Drule.types_sorts;

qualified inst;

qualified types_sorts, read_insts etc.;

Drule.types_sorts;

OldGoals.inst;

Drule.read_instantiate;

changed pred_congs: merely cover pred1_cong pred2_cong pred3_cong;

removed obsolete/unused pred_congs;

tuned comments;

converted ML proofs from simpdata.ML; tuned;

removed dead code;

RuleInsts.res_inst_tac with proper context;

more antiquotations;

tuned;

explicit rule for induct_tac

tuned spacing;

updated generated file;

* Attributes cases, induct, coinduct support del option.

added del attributes; tuned;

back to original import order -- thanks to proper deletion of nat cases/induct rules from type_definition;

proper deletion of nat cases/induct rules from type_definition;

fixed spelling (Where is WordExamples.thy anyway?);

recovered nat_induct as default for induct_tac;

more robust declaration of nat_induct;

reordering of imports ensures that nat_induct stay in front;

adhoc fix of induct_tac: rule nat_induct;

case_tac: accomodate change in bound variable name;

nat_induct_tac (works without context);

moved case_tac/induct_tac to induct_tacs.ML -- no longer hardwired into datatype package;

added nat_induct_tac (works without context);

InductTacs.case_tac with proper context and proper declaration of local variable;

added HOL/Tools/induct_tacs.ML;

eliminated obsolete case_split_thm -- use case_split; added case_split_tac (works without context); setup for induct_tacs.ML;

tuned proofs -- case_tac *is* available here;

updated generated file;

case_tac/induct_tac: use same declarations as cases/induct;

proper news header; methods case_tac and induct_tac now refer to usual declarations; removed obsolete induct_tac and thm_induct_tac;

removed obsolete read_idents;

added (e)res_inst_tac; tuned comments;

focus: actually declare constraints for local parameters;

tuned proofs;

case_split_tac (works without context);

tuned;

eliminated obsolete case_split_thm -- use case_split;

Unstructured induction and cases analysis for Isabelle/HOL.

dropped instance with attached definitions

polished interface of datatype package

adjusted some proofs involving inats

refactoring; addition, numerals

more instantiation

whitespace tuning

localized Least in Orderings.thy

removed some dubious code lemmas

slightly tuning of some proofs involving case distinction and induction on natural numbers and similar

rep_datatype command now takes list of constructors as input arguments

major refactorings in code generator modules

updated

slightly tuning of some proofs involving case distinction and induction on natural numbers and similar

DatatypePackage.case_tac;

DatatypePackage.distinct_simproc;

DatatypePackage.case_tac;

signature cleanup -- no pervasives anymore;

qualified DatatypePackage.distinct_simproc;

adapted case_tac/induct_tac;

updated generated file;

minor typos;

simp: depth_limit is now a configuration option;

removed old AxClass;

remove codegen_process.pdf from distribution;

fixed wrong treatment of type variables in instantiation target

switched to Poly/ML 5.2;

doc test now runs on linux

added at-poly-5.1-para-e;

adjusted location of cambridge website

switch from gtar to tar

send from linux systems as well

tikz: change to pgfsys-dvi.def for plain dvi output;

replaced (*<*)(*>*) by invisibility tags;

updated generated file;

updated generated file;

work within *this* directory;

moved labels into actual sections;

removed TEXPATH, just chdir to Locales/document;

renamed expression: plain ~ (space) instead of \colon;

updated generated file;

replaced strange \: by \colon to make it work again on macbroy20-29;

updated generated file;

clarification of "subst" by Lucas Dixon;

use polyml-5.2;

updated to official 5.2;

use isabelle style files from Doc/ -- not the generated ones (which are not present in the repository anyway);

some reorganization and fine-tuning;

some fine-tuning;

CodeTarget.target_code_width;

Tuned proof.

New version covering interpretation.

proper path to isabelle.jar;

reorganized isar-ref;

added Wenzel:2006:Festschrift;

class_deps: improper;

\cite{Wenzel:2006:Festschrift};

updated generated file;

moved stuff from pure.thy to Misc.thy;

obsolete;

updated generated file;

tuned;

updated generated file;

moved header command to Document_Preparation;

tuned structure;

moved header command here;

removed onsolete pure.thy (cf. Misc.thy);

updated generated file;

updated ML types for advanced translations;

moved (ax_)specification to end;

moved subst/hypsubst to "Basic proof tools"; tuned;

added Document_Preparation;

updated generated file;

tuned spacing;

major reorganization of document structure;

removed obsolete basics.tex;

more contributors; removed obsolete basics.tex; added Document_Preparation.tex;

renamed theory "syntax" to "Outer_Syntax";

isatool tty;

renamed theory "intro" to "Introduction";

tuned proofs

fixed bug: maxidx was wrongly calculuated from term, now calculated from theorem correctly.

new example

updated to E 0.999-006;

THIS_IS_ISABELLE_MAKEBIN is back;

cvs2cl only for unofficial releases;

more AFP sessions;

*** empty log message ***

Updated function tutorial.

(adjusted)

various code streamlining

more AFP sessions;

legacy_feature: no proof context in simpset;

proper context for attribute simplified;

added warning_count for issued reconstruction failure messages (limit 10); less nesting of let expressions;

proper context for ss;

proper context for simp_thms_conv;

added warning_count for issued reconstruction failure messages;

tuned;

*** empty log message ***

yet another attempt to circumvent printmode problems

obsolete;

moved README-polyml to polyml/README;

README for Poly/ML 5.2 distribution;

tuned;

more contribs;

misc tuning for Isabelle2008;

added some notable improvements;

tuned version numbers;

prepared for Isabelle2008;

added ISABELLE_HOME to startup; pathed OS.FileSys.tmpName to drop C string terminator; added OS.FileSys.fullPath;

added Substring.full;

moved distinctness_limit to datatype_rep_proofs.ML

fixed utterly wrong print mode handling

new serializer interface

added new code_datatype example

proper use of the Pretty module

permissive wrt. instantiation of class operations

proper lemma [source] antiquotation

check for illegal merge of class parameters

proper NoSubsort CLASS_ERROR

tuned theorem order

inst_subst_tac: match types -- no longer assume that subst rule has exactly one type argument; misc tuning -- more cterm operations, more qualified names;

updated generated file;

added local_theory command wrappers;

uniform treatment of target, not as config;

more uniform treatment of OuterSyntax.local_theory commands;

updated generated file;

invisible comment;

function: uniform treatment of target, not as config;

added parse_document (optional unchecked header material); parse: parse_document instead of parse_element;

exported master_directory;

present_excursion: setmp_thread_position during presentation;

use: explicit .ML;

ident: naive caching prevents potentially slow external invocations; tuned comments; tuned;

fixed improper handling of return code (pdf and ps.gz formats)

add constants: set Markup.theory_nameN in tags;

added theory_nameN;

rearranged subsections

Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that set print_mode and margin appropriately.

Replaced Pretty.str and Pretty.string_of by specific functions that set print_mode and margin appropriately.

temporary adjustment

tuned

more permissive preprocessor

explicit type schemes for functions

moved case distinction over number of constructors for distinctness rules from DatatypeProp to DatatypeRepProofs

added code for quantifiers

simplified proof

made the naming of the induction principles consistent: weak_induct is induct and induct is strong_induct

use_file: added str_of_pos argument (ignored);

Added entry explaining incompatibilities introduced by replacing sets by predicates.

instantiation lift :: (countable) bifinite

use new class package for classes profinite, bifinite; remove approx class

updated generated file;

unparse_term: check PureThy.old_appl_syntax instead of CPure;

theory Pure provides regular application syntax by default; added old_appl_syntax_setup for former Pure clients;

converted to regular application syntax;

eliminated theory CPure;

setup PureThy.old_appl_syntax_setup -- theory Pure provides regular application syntax by default;

* Eliminated theory ProtoPure and CPure, leaving just one Pure theory.

proper handling of the return code for the ps-format (fixes a bug)

oops -- pr_graph = Syntax.string_of_term; removed dead pr_matrix;

command 'normal_form': proper context via Variable.auto_fixes;

moved global pretty/string_of functions from Sign to Syntax; reordered signature;

Syntax.string_of_sort: proper context;

pprint: proper global context via Syntax.init_pretty_global;

Syntax.string_of_typ: proper context;

moved global pretty/string_of functions from Sign to Syntax; tuned message;

removed norm_absolute (not thread safe; chdir does not guarantee normalization anyway); full_path: no link expansion here (reverted change of 1.18); ident: OS.FileSys.fullPath takes care of link expansion;

renamed type decompT to decomp; refute: proper context for trace_ex; some attempts to improve readability;

Syntax.string_of_term with proper context;

moved global pretty/string_of functions from Sign to Syntax; removed dead code;

renamed type decompT to decomp;

pr_matrix: proper context;

guess_instance: proper context;

moved global pretty/string_of functions from Sign to Syntax;

tuned comments;

tuned proofs;

avoid undeclared variables in facts;

avoid undeclared variables within proofs; refrain from setting global references;

avoid undeclared variables within proofs;

tuned proof;

avoid undeclared variables within proofs;

cat_lines;

default token translations: observe Sign.is_pretty_global for fixed variables;

added pretty_global flag;

structure Display: less pervasive operations;

rename locales; add completion_approx constant to ideal_completion locale; add new set-like syntax for powerdomains; reorganized proofs

added a lemma about existence of contexts

* Method "cases", "induct", "coinduct": removed obsolete "(open)" option; * Isar statements: removed obsolete case "rule_context";

removed obsolete option open; tuned comments;

removed unused make_simple;

removed obsolete case rule_context;

fix looping simplifier

tuned;

tuned comment;

updated version;

removed unnecessary/untrusive a4paper option;

use Isabelle sty files from Doc/;

removed obsolete \ifpdfoutput;

* Simplified pdfsetup.sty;

use Isabelle sty files from Doc/;

updated generated file;

use Isabelle sty files from Doc/;

tuned clean_name (underscore);

load color/hyperref unconditionally; renamed color darkblue to linkcolor (default value unchanged); removed obsolete thumbpdf;

removed obsolete thumbpdf;

updated generated file;

use ../isabelle.sty, ../isabellesym.sty;

depend on ../pdfsetup.sty;

default linkcolor=black;

clean_name: replace "_" by "-";

updated generated file;

fixed some Isar element markups;

linkcolor=black (less noisy text);

hyperref is always enabled (also works with xdvi, dvips); replaced darkblue by generic linkcolor; reduced verbosity;

depend on ../pdfsetup.sty;

clean_string: cover <; added clean_name; output_entity: hyperlink;

updated generated file;

updated generated file;

proper checking of various Isar elements;

added defined_command, defined_option;

added intern, defined;

added defined;

setmp_thread_data: do nothing if Output.debugging;

names_of: exclude intermediate ids -- less verbosity;

remobed obsolete keyword concl;

explicit constraints for int literals;

use_text: added str_of_pos argument (ignored);

use_file: pass str_of_pos;

use_text/file: ignore str_of_pos argument;

use_text/file: proper position output;

renamed Position.path to Path.position; added line_file, ignore empty name;

renamed Position.path to Path.position;

load seq.ML and position.ML earlier;

adapted PolyML.compiler to latest change of basis/FinalPolyML.sml (2008-04-21);

fixed makefile