added boolN;

proper variant names (admit field "r");

three easy new examples

tuned footnote;

HOL/record: fixed select-update simplification procedure to handle extended records as well;

var: skolem;

remove *.out;

renamed Univalent to univalent

simplified some proofs

new examples that cannot be done in LEO

A few lemmas and some Adds.

Added global let-simplification rule.

Commenst.

added instance declaration for finite product

added split_eta_SetCompr, SetCompr_Sigma_eq

added Suc_le_D

added domI, domD

changed precedence of function update

installed lin arith for nat numerals.

Rename: theory for applying a bijection over states to a UNITY program

new distributive laws

expandshort

many new theorems about inj, surj etc.

new theorem nat_diff_split'

New treatment of "guarantees" with polymorphic components and bijections. Works EXCEPT FOR Alloc.

Syntax translation functions;

fixed some overfull lines

a smaller point size reduces the number of overfull figures

cosmetics

fixed sel_upd simproc (less efficient, but more complete);

lightweight bytecode verifier with correctness proof

basic source deps;

easy_setup: fixed mksimps;

proof step: reset goal_facts;

mkdir -p $ISABELLE_BROWSER_INFO;

fixed prefer;

tuned msg;

added refine_end; res_inst tactic emulation;

tuned attrib;

apply: observe facts; apply_end;

prf_script commands made proper; removed then_apply; added apply_end;

refine_end;

attrib: keyword_symid; goal_spec;

\isabellesimplestyle;

symid: include single symbolic char;

is_symbolic;

theorems [elim??] = sym;

added easy_setup;

add_judgment;

new thm and simprule inv_id

Cambridge-specific modifications

mirror dist page;

tuned;

mirror main page;

clearer "Obtaining" section

[df]rule methods;

document -c;

eliminated gif dir;

option -c;

updated the Client example