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

tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2

new thm order_less_imp_le

(then_)tac: assert_backward;

added -c option (beware!); changed default DIR to 'document'; NOTE: please ignore last log entry;

rename -p to -P; fixed target name: LOGIC-NAME;

added forget_proof;

added K.qed_global;

omit Primes;

(then_)apply: prove -> prove;

assert_no_chain;

refine_no_facts: recover goal_facts;

tuned prefer/defer;

intro/elim/dest attributes: changed ! / !! flags to ? / ??;

paper available

tidied some proofs

Branch: top elements of stack only need to be convertible (not equal)

tuned;

-I option;

-D PATH: dump generated document sources into PATH;

additional tex dump;

'.' == by this;

misc improvements;

added MicroJava/document;

added old_symbol_source; tuned;

Present.old_symbol_source;

tuned;

manually load session;

tuned syms;

new theorem gcd_add_mult

most_general_varify_tfrees all results;

Rduced Class C <= Class D to C <= D.

nat as names; obtain; tuned;

expandshort

new lemma fun_cons_restrict_eq

new theorems by Sidi O. Ehmety

added forgotten definition of make_imp_tac

added forgotten rules to make IMPP

eliminated nonascii;

added IMPP to HOL

renamed image_Union_eq -> image_Union

new theorem vimage_Union

new theorem rev_ImageI

various theorems about image and inverse image

Pi_empty1 is a more general simprule than empty_fun

rm -f *.aux;

simp_all method;

eliminated proof script;

HEADGOAL;

added prefer, defer;

added HEADGOAL;

added defer, prefer;

Drule.instantiate;

cp -r;

-p option;

added range_composition (also to simpset)

added finite_range_updI, finite_range_map_of, finite_range_map_of_override added, also to simpset: override_upd, ran_empty'

mkdir: prepare logic session directory;

added full_nat_induct

added splitE', also to claset

added inj_singleton

added finite_range_imageI