GENERATED TEXT;

fixencoding - fix references to isabelle font encoding;

tuned comments;

misc improvement;

Setup GNU Emacs for Isabelle environment.

tuned;

fixed { ... } shell syntax to accomodate bash 2.x;

Yet more fast_tac->blast_tac, and other tidying

tuned error msg;

Updated discussion and references for inductive definitions

Deleted stupid proof at the end not needed anywhere.

Mod because of "Turned Addsimps into AddIffs for datatype laws."

Turned Addsimps into AddIffs for datatype laws.

Changed some fast_tac to blast_tac

Added trace output and replaced fast_tac set_cs by Fast_tac.

replaced 'addwrapper' and 'addWrapper' by correct 'compwrapper' and 'compWrapper'

Thorough update.

Using Blast_tac

Control over excessive branching by applying a log2 penalty Incorporation of debugging features Allows backtracking over haz rules if alternatives exist Subsitution for equality may more a rule from the haz to the safe part

Explicit depth bounds seem necessary

Using Blast_tac

Dependency on Provers/nat_transitive

Couldn't solve n < n+1 because of missing -1

Dep. on Provers/nat_transitive

added -t (run tests) option;

added -g, -h options; replaced ISABELLE_HTML by ISABELLE_USEDIR_OPTIONS;

tuned xdvi invocation;

replaced ISABELLE_HTML by ISABELLE_USEDIR_OPTIONS;

improved messages;

fixed diagnostic output of print modes;

moved inj and surj from Set to Fun and Inv -> inv.

Inv -> inv

*** empty log message ***

Added Example Quot CVS ----------------------------------------------------------------------

Start Example

inv -> inverse

Example for higher order quotients: Fractionals

(higher-order) quotient constructor quot, based on PER

(partial) equivalecne relations. classes er<per

Inv -> inv

added -b option (batch mode);

renamed variable 'inv'

added Quot examples;

*** empty log message ***

Higher-order quotients.

Now calls blast_tac

Another blast_tac call

Simplified a proof

Re-organization of the order of haz rules

Calls Blast_tac. Tidied some proofs

Calls Blast_tac. Tidied some proofs

Calls Blast_tac

Adds image_eqI instead of imageI, as the former is more general

Added blast.ML as a dependency

Now calls Blast_tac and has some hard examples (Halting Problem

Only layout mods.

Now: unit = {True}

Two extra commands shorten the proof time by 800 seconds...

More List and ListPair utilities

Now exports declConsts! Temporarily erased target signature to aid debugging

Declares overloading for if-and-only-if

Declares overloading for set-theoretic constants

Removed (Unit) in Prod. Added test for ancestor Nat in datatype.

misc improvements;

changed signature of dummy goal from proto_pure to pure;

Converted to call blast_tac. Proves theorems in ZF.thy to make that theory usable again

Uses ZF.thy again, to make that theory usable

Mostly converted to blast_tac

Datatype declarations now require theory Datatype--NOT in quotes

Converted back from upair.thy to ZF.thy

Moved definitions (binary intersection, etc.) from upair.thy back to ZF.thy

Now checks for existence of theory Inductive (Fixedpt was too small)

Now a non-trivial theory so that require_thy can find it

DEEPEN now takes an upper bound for terminating searches

New DEEPEN allows giving an upper bound for deepen_tac

Now builds blast_tac

Now loads blast.ML

ZF.thy is again usable

The isabelle-0 encoding table.

Made the error message more explicit

Now declares Basis Library version of type option Also function mapPartial

Replaced Best_tac by the one rule needed for the proof

Installation of blast_tac

Now tests for essential ancestors (Lfp or Gfp)

Re-ordering of rules to assist blast_tac Powerset rules must not be the most recent

Now loads blast_tac

Reorganization of how classical rules are installed

Now calls require_thy to ensure ancestors are present

Implementation of blast_tac: fast tableau prover

replaced by usedir;

eliminated references to old 8bit fonts;

improved messages;

removed useless symbol font syntax;

fixed -s option;

simple_ast_of: fixed handling of loose Bounds;

Replaced (s,t) : id by s=t.

Optimized proofs.

Changes made necessary by the new ex1 rules

Now uses the alternative (safe!) rules for ex1

Updated comment

Cleaned up a little.

Added "discrete" CPOs and modified IMP to use those rather than "lift"

generalized theorems and class instances for Cprod. Now "*"::(cpo,cpo)cpo and "*"::(pcpo,pcpo)pcpo

changed some theorems from pcpo to cpo

changed continuous functions from pcpo to cpo (including instances)

Trivial renamings (for consistency with CSFW papers)

Toby's better treatment of eta-contraction

Deleted needless parentheses

Deleted unnecessary rules

fixed font names;

exit_use_dir; tuning;

isatool usedir;

exit_use_dir;

remove empty dirs;

isatool usedir;

improved session names;

isatool usedir;

*** empty log message ***

tuned;

isatool usedir;

exit_use_dir;

isatool usedir;

replaced ex.ML by ex/ROOT.ML, ex/ex.ML;

isatool usedir;

added ex dir;

replaced ex.ML by ex/ROOT.ML, ex/ex.ML;

replaced ex.ML by ex/ROOT.ml, ex/ex.ML;

Improved intersection rule InterI: now truly safe, since the unsafeness is delegated to exI.

delete_tagged_brl just ignores non-elimination rules instead of complaining

delrules now deletes ALL occurrences of a rule, since it may appear in any of the four lists.

added quit();

asserts $ISABELLE_OUTPUT_DIR;

Added wp_while.

added dummy set_session;

usedir -- build object-logic or run examples;

A more explicit prefix because gensym now generates easily predicatable identifiers

gensym no longer generates random identifiers, but just enumerates them starting from A. The random number generator was needlessly slow and caused portability problems.

Made the indentation rational

fixed Tools path;

Conducted the IFOL proofs using intuitionistic tools

Stopped giving Introduction rules as Elimination rules

Added P&P&Q <-> P&Q and P|P|Q <-> P|Q

Added P&P&Q = P&Q and P|P|Q = P|Q.

*** empty log message ***

The HOLCF-based den. sem. of IMP.

Added the HOLCF-based den. sem. of IMP.

Added link to HOLCF/IMP

fixed perl path;

uncommented chown / chmod (again);

Modified proofs because simplifier does not eta-contract any longer.

Avoid eta-contraction in the simplifier. Instead the net needs to eta-contract the object. Also added a special function loose_bvar1(i,t) in term.ML.

tuned glyphs;

tuned Sigma glyph;

major tuning;

tuned comments; added -h option;

tuned comments; added ISABELLE_TOOLS support;

tuned comments;

tuned;

tuned comment; more robust check;

Note on fonts and remote X11;

tr is (again) type abbrev;

added THIS_IS_ISABELLE_BUILD;

added THIS_IS_ISABELLE_BUILD discrimination;

The contr_tac, which replaces a fast_tac, is needed only because eq_assume_tac does not recognize eta-equality. But making it do so is costly

renamed;

fixed;

commented out chwon, chmod;

fixed src path;

added \n at EOF;

*** empty log message ***

tuned;

renamed fonts;

renamed font;

removed lparr, rparr, empty, succeq, ge, rrightarrow; added turnstile, Turnstile, cdot, approx, Colon, bow; renamed tick to surd;

renamed SYSTEM to RAW_ML_SYSTEM;

added \<Colon> syntax for constraints (more compact!);

"bool lift" now syntax instead of type abbrev;

*** empty log message ***

added atac 2 (again);

removed (| |) symbols syntax;

fixed Not syntax;

tuned comment;

tuned comments;

Isabelle installation notes;

now sans serifs;

tuned;

*** empty log message ***

build - compile parts of the Isabelle system;

moved settings comment to build;

Removed some polymorphic equality tests

Improved indentation of aconv

Corrected aeconv and exported it

Prevent permutation of assumptions in hyp_subst_tac

Deleted steps made redundant by the stronger eq_assume_tac

Eta-expanded some declarations for compatibility with value polymorphism

Tidied and updated

more robust check;

renamed, improved, augmented version of isabelle fonts;

tuned comment;

tuned;

pass xterm mode by default;

Minor changes due to primrec definition for ^

primrec definition for ^

Minor changes due to primrec definition for nth

primrec definition for nth

Oops, forgot to remove -x again;

added ISABELLE_HOME normalization;

even more robust and user friendly invocation (no longer requieres absolute path names);

improved DESCRIPTION;

added -a, -b options; multiple VARNAMES;

*** empty log message ***

*** empty log message ***

*** empty log message ***

Added comment

Now uses eta_contract_atom for greater speed

Eta-expanded declarations of addSIs2, etc., to avoid polymorphism errors

HOL: renaming of "not"

Declares eta_contract_atom; fixed comment; some tidying

Added comment

Now declares needs_filtered_use, but still unusable with current MLWorks

Now uses rotate_tac and eta_contract_atom for greater speed

New version of InterE, like its ZF counterpart

Renamed constant "not" to "Not"

Renamed constant "not" to "Not"

Renamed constant "not" to "Not"

best_tac avoids looping with change to RepFun_eqI in claset

Now uses RepFun_eqI instead of RepFunI; improved version of InterE to replace "make_elim InterD" in claset

Updated reference to Pelletier erratum

Removed needless quotes

removed bash debug;

removed -r option; added -p option;

fixed -m order;

improved xterm, xterm_color;

added comment;

added comment: print translations do not mark tokens;

added color styles; refs for test;

improved err msg;

*** empty log message ***

more robust handling of invocation errors; added -m MODE option;

more robust handling of invocation errors;