src/HOL/MicroJava/BV/BVSpec.thy
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2002-06-14 kleing 2002-06-14 wt_method now checks bounded+types ==> wt_kildall <=> wt_method
2002-03-03 kleing 2002-03-03 symbolized
2002-02-21 kleing 2002-02-21 new document
2001-12-16 kleing 2001-12-16 exceptions
2001-02-09 kleing 2001-02-09 tuned for 99-2 release
2001-02-01 oheimb 2001-02-01 converted to Isar, simplifying recursion on class hierarchy
2001-01-18 oheimb 2001-01-18 is_class and class now as defs (rather than translations); corrected Digest.thy
2000-12-10 kleing 2000-12-10 moved method lemma to BVSpec
2000-12-07 oheimb 2000-12-07 removed two intermediate comments
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 fixed document preparation
2000-12-05 kleing 2000-12-05 BCV Integration
2000-11-20 kleing 2000-11-20 BCV integration (first step)
2000-09-21 kleing 2000-09-21 unsymbolized
2000-08-30 kleing 2000-08-30 functional LBV style, dead code, type safety -> Isar
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 ADD -> IAdd
2000-07-06 kleing 2000-07-06 new ADD instruction
2000-03-09 kleing 2000-03-09 minor adjustments in branch and method invocation for completeness of LBV
2000-02-05 kleing 2000-02-05 Branch: top elements of stack only need to be convertible (not equal)
1999-12-06 nipkow 1999-12-06 Renamed some vars
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-19 oheimb 1999-11-19 re-shaped and re-ordered conversion relations
1999-11-11 nipkow 1999-11-11 *** empty log message ***