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;