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

NEWS about measure functions

updated generated file;

Measure functions can now be declared via special rules, allowing for a prolog-style generation of measure functions for a specific type.

misc tuning;

updated generated file;

fixed some labels;

avoid old macros from isar.sty;

misc reorganization;

added chapters for "Specifications" and "Proofs";

removed outdated comment;

updated generated file;

proper antiquotations for commands;

removed obsolete macros for Isar commands etc.; tuned;

replaced macros by antiquotations;

removed obsolete macros for Isar commands etc.;

added local copy of underscore.sty;

updated generated file;

replaced some latex macros by antiquotations;

removed obsolete macros; tuned;

removed obsolete math macros;

depend on style.sty;

updated generated file;

depend on ../../antiquote_setup.ML;

improved treatment of "_" thanks to underscore.sty;

clean_string: map "_" to "\\_" (best used with underscore.sty);

misc tuning;

slight tuning of the 1st paragraph

unused;

converted HOL specific elements;

added rail setup for verblbrace, verbrbrace;

added at_set_avoiding lemmas

removed obsolete conversion guide -- converted only section on tactics;

converted ZF specific elements;

enabled ThyOutput.source option by default;

output_entity: ignore ThyOutput.source option;

updated generated file;

converted HOLCF specific elements;

added logic-specific sessions;

Updated.

Instantiated rule increasing_chain_adm_lemma in proof of flatstream_adm_lemma to avoid problems with HO unification.

Replaced instance declarations for sets by instance declarations for bool. Together with the instance declarations for fun from Ffun, this subsumes the old instance declarations for sets.

Adm now imports Ffun rather than Cont, because SetPcpo, which imports Adm, needs functions (since sets are now just functions).

Lookup and union operations on terms are now modulo eta conversion.

Terms returned by decomp are now eta-contracted.

Added function for computing instantiation for the subst rule, which is used in vars_gen_hyp_subst_tac and blast_hyp_subst_tac to avoid problems with HO unification.

eq_assumption now uses aeconv instead of aconv.

- Removed function eta_contract_atom, which did not quite work - Corrected and simplified function aeconv

Replaced Pattern.eta_contract_atom by Envir.eta_contract.

Removed instantiation for set.

Explicitely applied ext in proof of tnd.

Deleted subset_antisym in a few proofs, because it is accidentally applied to predicates as well.

- Tuned imports - Replaced blast by simp in proof of Stable_final_E_NOT_empty, since blast looped because of the new encoding of sets.

Manually applied subset_antisym in proof of Compl_fixedpoint, because it is accidentally applied to predicates as well.

Replaced blast by fast in proof of INT_Un_Compl_subset, since blast looped because of the new encoding of sets.

Functions get_branching_types and get_arities now use fold instead of foldl/r.

Temporarily disabled invocations of new code generator that do no longer work due to the encoding of sets as predicates

Replaced instance "set :: (plus) plus" by "fun :: (type, type) plus"

- Deleted arity proofs for set - Produce specific instances of theorems insert_eqvt, set_eqvt and perm_set_eq

Replaced union_empty2 by Un_empty_right.

Instantiated rule expand_fun_eq in proof of set_of_eq_empty_iff, to avoid that it gets applied to sets as well.

Deleted instance "set :: ({heap, finite}) heap"

- Declared subset_eq as code lemma - Deleted types_code declaration for sets

Deleted instantiation "set :: (enum) enum"

Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with definitions of + and * on functions.

Rephrased calculational proofs to avoid problems with HO unification

Rephrased forward proofs to avoid problems with HO unification

Rephrased proof of ann_hoare_case_analysis, to avoid problems with HO unification

Locally deleted some definitions that were applied too eagerly because of eta-expansion

- Instantiated parts_insert_substD to avoid problems with HO unification - Replaced auto by fastsimp in proof of parts_invKey, since auto looped because of the new encoding of sets

Instantiated parts_insert_substD to avoid problems with HO unification

Replaced blast by fast in proof of parts_singleton, since blast looped because of the new encoding of sets.

Adapted to encoding of sets as predicates

Replaced forward proofs of existential statements by backward proofs to avoid problems with HO unification

Adapted functions mk_setT and dest_setT to encoding of sets as predicates.