src/HOL/MicroJava/BV/Typing_Framework_JVM.thy
2010-03-01 ago replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2009-11-24 ago backported parts of abstract byte code verifier from AFP/Jinja
2009-11-12 ago New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
2009-09-21 ago tuned proofs
2008-03-27 ago avoid amiguity of State.state vs. JVMType.state;
2008-03-15 ago avoid unclear fact references;
2005-08-17 ago small mods to code lemmas
2005-06-17 ago migrated theory headers to new format
2003-05-26 ago Introduced distinction wf_prog vs. ws_prog
2002-09-30 ago Adapted to new simplifier.
2002-06-19 ago LBV instantiantion refactored, streamlined