added is_unitT; added proper versions of mk_tuple(T), dest_tuple(T) -- unused;

instance unit :: finite;

more robust tuple syntax (still improper, though!);

improved unit theory: unit_all_eq1, unit_all_eq2, split_all_tac; tuned;

added syntax for proper / improper selector functions;

tuned;

tuned;

avoid 'split';

added Tuple.thy;

added ex/Tuple.thy;

syntax (symbols) "op o" moved from HOL to Fun;

added finite_unit;

AST translation rules no longer require constant head on LHS;

* tuned AST representation of nested pairs, avoiding bogus output in case of overlap with user translations (e.g. judgements over tuples); * AST translation rules no longer require constant head on LHS;

corrections (cast relation, Prog.ML -> Decl.ML)

improved add_edges_cyclic;

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;