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