modernized header;
removed junk;
non-executable source files;
backported parts of abstract byte code verifier from AFP/Jinja --HG-- extra : rebase_source : 1d943bc92831d0a92004a43f72ff37eb352bf23f
tuned size of included graph;
fix toc
new document
include document graph;
tuned
tuned, added lightweight BV to abstract, added Bali link
*** empty log message ***
added mJava macro
added latexsym (no longer loaded by isabellesym);
added title, abstract, bibliography;
improved section markup;
added MicroJava/document;