Old ABP files now running under the IOA meta theory based on HOLCF;

New meta theory for IOA based on HOLCF.

improved display of non-ASCII chars;

fixed enc_start;

deactivated new symbols (not yet printable on xterm, emacs);

renamed \<choice> to \<orelse>;

added \<orelse> symbols syntax for case;

added \<langle>, \<rangle> symbols syntax;

added new chars;

is_blank: added space2 (160);

improved DVI_VIEWER default;

improved tmp comment;

removed -norc;

used explcite tactics in instances (since ax_per_trans "loops")

changed Domain->Dom for SML/NJ

removed -c option;

removed -c option;

removed COPYDB flag;

removed -c option;

obsolete;

no longer forces default;

misc tuning;

removed one blank at end of line 37

refer to SOME, NONE on top-level;

adapted for 1.09.27 (and later);

open General (type option is in Option in the newer versions, but always the top-level);

adapted to SML/NJ 1.09.27; minor cleanup;

Added 'induct_tac'

Updates because nat_ind_tac no longer appends "1" to the ind.var.

removed space;

induct_tac

expandshort

Introduced a generic "induct_tac" which picks up the right induction scheme automatically. Also changed nat_ind_tac, which does no longer append a "1" to the name of the induction variable. This caused some changes...

get_thydata accesses the second component of the data field. This component used to be empty until set at the end of loading an ML file. Now the second component is already set when the thy file has ben read.

Main changes are: - Lemmas for blift and plift are deleted - added split_tac for If (via If2, as If does not begin with a constant) - added new lemmata relating TT, FF and booleans: Def_bool1, Def_bool2, Def_bool3,Def_bool4 They are added to !simpset, but should not cause difficulties - added lemma andalso_or relating | on booleans and andalso on truth values - deleted If_and_if and andalso from !simpset: Pay attention, may kill your proofs! - added adm lemmas for (f x)~=TT and (f x)~=FF.

rename_params_rule used to check if the new name clashed with a free name in the whole goal state. Now checks only the subgoal concerned.

deleted definitions for blift and plift

Complete Redesign of Theory, main points are: - Extension of the continuity prover: * Lemmas about continuity of flift1 and flift2 are generalized * Lemmas about continuity of mixed definitions of HOL and LCF terms generalized Pay attention: Sometimes proofs are shorter now! - a number of new lemmas concerning flift1, flift2, Def and Undef, Def_less_is_eq (Def x << y = (Def x = y)) and lemmas characterizing flift1 and flift2 are added to !simpset Pay attention: Sometimes proofs are shorter now! - added tactic def_tac for eliminating x~=UU in assumptions

added liftpair definition

only in comments

minor changes due to more powerful continuity check in Lift3.ML

added some comments;

Addition of printed tracing. Also some tidying

A bit of tidying

added dependencies on ax_ops/*.ML and domain/*.ML

changed priority of '%': now no parenteses needed for '[...] == %x. [...]'

moved antisym_less_inverse,box_less from Porder.ML to Porder0.ML

Added NatDef

Necessary inclusion of depth bound into blast_tac call

Ran expandshort

Unfortunately, the \\< syntax does not always accept the beginning of a line

Loop detection: before expanding a haz formula, see whether it is a duplicate and, if so, delete it. Recursion detection: transitivity and similar rules, when applied, put the new formulae at the end of a branch and not at the front (in effect).

Made a proof search more deterministic

Improved indentation of #34

Ran expandshort

Fixed typos in comment

Conversion to use blast_tac

Ran expandshort

Moved diamond_trancl (which is independent of the rest) to the top

Ran expandshort

simprocs called with eta contracted subterm;

Tidied up.

fixed bash-2.0 problem;

improved fontserver example;

Ran expandshort

removed -norc;

tuned;

Modified credits.

New elimination rule for "unique existence"

New introduction rule for "unique existence"

Reorganized under headings. Also documented Blast_tac and LFilter

Tidied up the indentation

Moved blast_tac demo from ZF/func.ML to ZF/ex/misc.ML

Penalty for branching instantiations reduced from log3 to log4. Now allows a branch to close by unifying an OConst with a Const.

New blast_tac demo

Without the type constraint, the inner equality was NOT a biconditional...

Now faster without calling Blast.depth_tac

Disabled the attempts for mutual induction to work so that single induction involving sum types can work

Tuple patterns are allowed now in `case'

*** empty log message ***

print_goals: fixed show_sorts semantics;

tuned check_has_sort; fixed norm_typ: also does norm_sort;

removed least_sort; added of_sort;

tuned err msg;

Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy

Now loads theory LList indirectly: via LFilter

Now uses some "case" syntax (but could use more)

New monotonicity theorems

New theory: a corecursive filter functional

Removed needless parentheses from translation

ex/LFilter is a new theory (and dependency)

Automatic update

tuned error msgs;

improved type check error messages;

renamed set_ap to setmp;

Automatic updates

Removed the \date{} command in order to put the date of typesetting on the title page

Corrected the informal description of coinductive definition

Corrected the informal description of coinductive definition in sections 1 and 4.3, introducing the notion of "consistent with" a set of rules. Final version for Milner Festschrift?

Added ability to have case expressions involving tuples. (via translation)

tuned;

*** empty log message ***

added fixencoding note;

fixed ISAMODE_HOME;

eliminated PLATFORM;

removed lceil, rceil, lfloor, rfloor;

fixed perl path (for sunbroys);

improved translations for subset symbols syntax: constraints;

moved classes / sorts to sorts.ML; moved (and reimplemented) type inference to type_infer.ML; cleaned up type unification; misc cleanup and tuning;

renamed subclass to classrel; tune type checking error msgs;

Sorts.str_of_sort;

Sorts.str_of_arity;

added sorts.ML, type_infer.ML;

tuned type of eq_ix, mem_ix;

improved inc, dec; added set_ap;

Type inference (isolated from type.ML, completely reimplemented).

Type classes and sorts (isolated from type.ML).

improved;

Partially converted to call blast_tac

Addition of blast_tac benchmark

Changed penalty from log2 to log3

An extra call to blast_tac (illustrating a need for type instantiation)

Now puts basic rewrites for lappend & lmap into the simpset

Removed "AddSDs [Scons_inject];" because (a) IT WAS WRONG (should have been AddSEs) (b) It was redundant (due to the AddIffs [...,Scons_Scons_eq])

Moved expand_case_tac from Auth/Message.ML to simpdata.ML

no longer includes ~/.emacs;

fixed file name;

GENERATED TEXT;

tuned format;

GENERATED TEXT;

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;