src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
2003-05-26 streckem 2003-05-26 Introduced distinction wf_prog vs. ws_prog
2003-05-14 nipkow 2003-05-14 *** empty log message ***
2002-11-16 kleing 2002-11-16 beautified "match"
2002-10-24 kleing 2002-10-24 changes for cleanup in JVM
2002-10-23 streckem 2002-10-23 Added compiler
2002-08-27 wenzelm 2002-08-27 *** empty log message ***
2002-03-09 kleing 2002-03-09 canonical start state
2002-03-03 kleing 2002-03-03 symbolized
2002-02-26 kleing 2002-02-26 introduces SystemClasses and BVExample
2002-02-21 kleing 2002-02-21 new document
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-12-05 wenzelm 2001-12-05 eliminated old use of intro/elim method; tuned;
2001-11-16 kleing 2001-11-16 fixed maxs bug
2001-04-12 kleing 2001-04-12 cleanup, tuned
2001-02-09 kleing 2001-02-09 tuned for 99-2 release
2001-01-16 kleing 2001-01-16 newref -> new_Addr
2001-01-14 kleing 2001-01-14 removed instructions Aconst_null+Bipush, introduced LitPush
2001-01-07 kleing 2001-01-07 merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
2001-01-02 oheimb 2001-01-02 added type annotation to Call
2000-12-07 kleing 2000-12-07 update for changes in Correct.thy and class/is_class defs
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-11-03 wenzelm 2000-11-03 adapted "obtain" proofs;
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-09-03 wenzelm 2000-09-03 tuned;
2000-08-30 kleing 2000-08-30 functional LBV style, dead code, type safety -> Isar
1999-11-11 nipkow 1999-11-11 *** empty log message ***