re-structuring MicroJava; added Example; corrected := syntax; simplfied cast

added (surjective_pairing RS sym) to simpset

strengthened rtranclD

added option_map_o_sum_case (also to simpset)

added sum_case_empty_empty (also to simpset)

tuned syntax

added hint on fun_sum

added fun_upd2_simproc

re-added subset_empty to simpset

used bounded quantification in definition of guarantees and other minor adjustments

moved sublist from UNITY/AllocBase to List

AddIffs

parent should be Main

changed the quotient syntax from / to //

tuned cycle_msg;

updated;

HOL: the disjoint sum is now "<+>" instead of "Plus"; ML: PureThy.add_defs gets additional argument;

adapted PureThy.add_defs_i;

defs (overloaded);

tuned;

added read_xnum;

fix(_i): admit internal variables;

use ProofContext.bind_skolem;

defs: (overloaded) option;

eq_prop: strip_assums_concl;

tuned exceptions; added add_deps_acyclic, merge_acyclic;

const_deps: unit Graph.T; proper merge of const_deps; tuned;

add_term_consts: ins_string;

add_defs(_i): overloaded option;

adapted PureThy.add_defs;

fixed comment;

adapted PureThy.add_defs_i;

use Syntax.read_xnum;

fixed simplified_cases;

fixed name: UN_empty3;

replaced infix Plus by <+>;

removed duplicate Compl_atMost;

fixed compose decl;

defs: (overloaded) option;

method cases/induct: (opaque) option;

defs (overloaded);

removed now-redundant proof steps

added an important default rule

fixed a failing proof

le_refl_iff as default rule

removed needless premises

AddIffs now available for FOL, ZF

added simp_case_tac; proper handling of case names with simplification; support "(opaque)" mode; tuned;

use InductMethod.simp_case_tac;

tuned;

export thesisN separately;

prep rhs in original context; tuned;

RuleCases.make opaq;

bind_skolem;

invoke_case: bind_skolem;

"_i" arguments now expected to have skolems already internalized; removed unused cert_skolem, export intern_skolem, added bind_skolem;