tuned;

corrected header

changed / to // for quotienting

changed / to // for quotienting; general tidying

renamed // to / (which is what we want anyway) to avoid clash with the new use of // for quotienting

deleted redundant proof

// change; also moved entry for AddIffs

addsplits [split_if];

theorems foo.splits = foo.split foo.split_asm;

removed obsolete expand_if = split_if;

* HOL: removed obsolete expand_if = split_if; theorems if_splits = split_if split_if_asm;

* HOL: removed obsolete expand_if = split_if; theorems if_splits = split_if split_if_asm; datatype package provides theorems foo.splits = foo.split foo.split_asm for each datatype;

replaced arities by instance;

MicroJava structure changed

consts: include *all* names;

tuded presentation;

AddXIs [UnI1, UnI2];

flat instruction set, op. semantics now in JVMExecInstr.thy

flat instruction set

10pt

- xsymbols for \<noteq> \<notin> \<in> \<exists> \<forall> \<and> \<inter> \<union> \<Union> - vector space type of {plus, minus, zero}, overload 0 in vector space - syntax |.| and ||.||

strip_prod_type = HOLogic.prodT_factors;

AST translation rules no longer require constant head on LHS;

fixed nested prod syntax;

use split_tupled_all;

use pair_tac; use split syntax;

adapted tuple syntax;

tuned;

use pair_tac;

use split syntax;

fixed tuple translations;

defs (overloaded);