src/HOL/MicroJava/BV/LBVComplete.thy
2000-09-12 wenzelm 2000-09-12 renamed atts: rulify to rule_format, elimify to elim_format;
2000-09-07 wenzelm 2000-09-07 updated attribute names;
2000-08-30 kleing 2000-08-30 functional LBV style, dead code, type safety -> Isar
2000-08-20 wenzelm 2000-08-20 open cases;
2000-08-14 kleing 2000-08-14 Convert.thy now in Isar, tuned
2000-08-11 kleing 2000-08-11 tuned
2000-08-09 kleing 2000-08-09 tuned
2000-08-07 kleing 2000-08-07 BV and LBV specified in terms of app and step functions
2000-07-17 kleing 2000-07-17 flat instruction set
2000-07-06 kleing 2000-07-06 new ADD instruction
2000-06-28 kleing 2000-06-28 tuning, eliminated rev_surj
2000-06-07 kleing 2000-06-07 minor tuning for pdf documents
2000-05-31 kleing 2000-05-31 switched to Isar proofs
2000-03-09 kleing 2000-03-09 completeness of the lightweight bytecode verifier