??id syntax for text variables;

dest_binding, dest_skolem;

val single: 'a -> 'a list; val suffix: string -> string -> string; val unsuffix: string -> string -> string;

Tidying of AC, especially of AC16_WO4 using a locale

More lemmas about lex.

*** empty log message ***

List now contains some lexicographic orderings.

added store_tthm;

Improved well-formedness check.

even more tidying of Goal commands

A higher-level treatment of LeadsTo, minimizing use of "reachable"

Simplified proof!!

*** empty log message ***

Lemma renamed in HOL.

Added macro `termi'

New lemmas in List and Lambda in IsaMakefile

Removed duplicate thms (see comment to Arith.ML)

Removed duplicate thms: less_imp_add_less = trans_less_add1 le_imp_add_le = trans_le_add1

Removed comments.

even more tidying of Goal commands

disjointness

Now recognizes both {}= and ={}

Disjointness reasoning by AddEs [equals0E, sym RS equals0E] and consequential changes (and tidying)

New result from AC directory

added solve_tac;

New results from AC

First steps towards termination of simply typed terms.

binding / skolem vars;

Null program and a few new results

Finished the example

Indentation, comments

Renamed equals0D to equals0E

Tidied

Removal of "disjoint" translation

New record type of programs

Union primitives and examples

tuned; Display.print_goals function moved to Locale.print_goals;

added LocaleGroup, PiSets examples;

added Open_locale, Close_locale; thm(s): use Locale.get_thm(s);

added 'locale' section;

Locale.setup;

added export: thm -> thm; exported print_current_goals_default; locale support;

moved print_goals to locale.ML;

added locale.ML;

added icons;

Renamed equals0D to equals0E

Renamed equals0D to equals0E; tidied

Constant "invariant" and new constrains_tac, ensures_tac

Tidying

Boolean quantification

Deleted the redundant rule mem_if

fixed disjount translation;

tuned comments;

Better comments

New rewrite rules for quantification over bounded UNIONs

Tidied; uses records

new theorems for partial funcs

Pretty.sym;

size / length: printable length;

isatool expandshort;