src/HOL/MicroJava/BV/LBVComplete.thy
2008-12-16 ballarin 2008-12-16 More porting to new locales.
2008-07-25 haftmann 2008-07-25 dropped locale (open)
2007-06-21 wenzelm 2007-06-21 tuned proofs -- avoid implicit prems;
2007-06-21 wenzelm 2007-06-21 tuned proofs -- avoid implicit prems;
2007-06-06 nipkow 2007-06-06 changed filter syntax from : to <-
2005-08-17 nipkow 2005-08-17 small mods to code lemmas
2005-08-16 nipkow 2005-08-16 name fix
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2004-12-22 nipkow 2004-12-22 [ .. (] -> [ ..< ]
2002-07-16 wenzelm 2002-07-16 adapted to locale defs;
2002-04-30 kleing 2002-04-30 tuned
2002-04-04 kleing 2002-04-04 flattened, uses locales
2002-04-02 nipkow 2002-04-02 Started to convert to locales
2002-03-27 kleing 2002-03-27 finished lbv completeness
2002-03-26 kleing 2002-03-26 merge mono
2002-03-24 kleing 2002-03-24 cleanup + simpler monotonicity
2002-03-21 kleing 2002-03-21 first steps in semilattices..
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
2000-12-07 kleing 2000-12-07 fixed and cleaned up wt[l]_jvm_prog proofs
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-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-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