src/HOL/MicroJava/BV/Correct.thy
2002-10-27 kleing 2002-10-27 simplified lemma correct_frames_newref
2002-03-09 kleing 2002-03-09 canonical start state
2002-03-03 kleing 2002-03-03 symbolized
2002-02-21 kleing 2002-02-21 new document
2002-01-15 kleing 2002-01-15 fixed theory deps
2001-12-18 kleing 2001-12-18 removed preallocated heaps axiom (now in type safety invariant)
2001-12-16 kleing 2001-12-16 exceptions
2001-06-12 oheimb 2001-06-12 corrected xsymbol/HTML syntax
2001-04-12 kleing 2001-04-12 cleanup, tuned
2001-02-22 kleing 2001-02-22 removed unused constant
2001-02-09 kleing 2001-02-09 tuned for 99-2 release
2001-01-16 kleing 2001-01-16 newref -> new_Addr
2001-01-07 kleing 2001-01-07 merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
2000-12-07 kleing 2000-12-07 strengthened invariant: current class must be defined
2000-12-06 oheimb 2000-12-06 improved superclass entry for classes and definition status of is_class, class corrected recursive definitions of "method" and "fields" Beware: some proofs are incomplete (sorry, oops), preliminary comments with DvO:
2000-12-05 kleing 2000-12-05 BCV Integration
2000-11-20 kleing 2000-11-20 BCV integration (first step)
2000-09-22 kleing 2000-09-22 added HTML syntax
2000-09-21 kleing 2000-09-21 tuned spacing for document generation
2000-09-21 kleing 2000-09-21 unsymbolized
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-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-01-12 nipkow 2000-01-12 Move some lemmas to List.
1999-12-02 nipkow 1999-12-02 cosmetic mod.
1999-12-01 nipkow 1999-12-01 Fixed a problem with returning from the last frame.
1999-11-26 nipkow 1999-11-26 Various little changes like cmethd -> method and cfield -> field.
1999-11-25 nipkow 1999-11-25 Minor mods.
1999-11-11 nipkow 1999-11-11 *** empty log message ***