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;