*** empty log message ***

Isar_examples/W_correct moved to W0;

tuned;

converted;

added check_text;

export locale_target, locale_keyword;

markup commands moved to isar_cmd.ML;

updated markup commands; clarified syntax of ``long'' statements: fixes/assumes/shows;

export eval_antiquote;

markup commands (from isar_thy.ML) with proper check of antiquotations;

clarified syntax of ``long'' statements: fixes/assumes/shows;

clarify module dependencies;

updated;

Clarification wrt. use of polymorphic variants of Hoare logic rules

Introduced variants of operators + * ~ constrained to type int (to make SML/NJ happy).

updated debugging output

solved the problem that Larry's simproce cancle_numerals(?) returns inconsistent inequality w/o rewriting it to False.

added using_thmss(_i);

added using_facts;

replaced 'using' keyword by 'to';

tuned;

'using' command;

Added check for field/method access to operational semantics and proved the acesses valid.

* HOL: removed obsolete theorem "optionE";

fixed get_name_tags in order to work with hyps;

clarified internal theory dependencies;

bind_thms basic_monos;

include theory Record (tuned dependencies);

removed theory Option;

theory Option has been assimilated by Datatype;