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;