src/HOL/MicroJava/BV/JType.thy
2003-05-26 streckem 2003-05-26 Introduced distinction wf_prog vs. ws_prog
2002-04-02 nipkow 2002-04-02 Started to convert to locales
2002-03-03 kleing 2002-03-03 symbolized
2002-02-21 kleing 2002-02-21 new document
2002-01-15 kleing 2002-01-15 use exec_lub instead of some_lub
2001-12-16 kleing 2001-12-16 exceptions
2001-12-10 berghofe 2001-12-10 Turned subcls1 into an inductive relation to make it executable.
2001-02-09 kleing 2001-02-09 tuned for 99-2 release
2001-01-18 oheimb 2001-01-18 is_class and class now as defs (rather than translations); corrected Digest.thy
2001-01-14 kleing 2001-01-14 tuned
2001-01-07 kleing 2001-01-07 merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
2001-01-05 nipkow 2001-01-05 ^^ -> ``` Univalent -> single_valued
2000-12-07 kleing 2000-12-07 updated for is_class changes
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 (type system is semilattice)