isabelle update_cartouches -c -t;

isabelle update_cartouches;

modernized header;

prefer stateless 'ML_val' for tests;

modernized specifications;

replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed

replace old SML code generator by new code generator in MicroJava/JVM and /BV

replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)

backported parts of abstract byte code verifier from AFP/Jinja

--HG--
extra : rebase_source : 1d943bc92831d0a92004a43f72ff37eb352bf23f

temporary adjustment to dubious state of eta expansion in recfun_codegen

arbitrary is undefined

code example: back to individual ML commands, which are now thread-safe;

avoid internal names;

theory header: more precise imports;

dropped code generator setup garbage

tuned ML declarations;

consts in consts_code Isar commands are now referred to by usual term syntax

more robust syntax for definition/abbreviation/notation;

adapted to new serializer syntax

slight cleanup

added code generator setup

generated code: raise Match instead of ERROR;

Adapted to new code generator syntax.

Auxiliary functions to be used in generated code are now defined using "attach".

Corrected implementation of arbitrary on cname.

migrated theory headers to new format

tuned

wf is no longer implemented by true (due to change in definition of class_rec).

canonical start state

fixed missing label

introduces SystemClasses and BVExample

new document

cast_ok and match_exception_entry no longer disabled (thanks to
improvement of code generator).

fixed JVMListExample

exception merge, doesn't work yet

Example for code generator.