src/HOL/MicroJava/BV/BVExample.thy
2010-12-29 wenzelm 2010-12-29 explicit file specifications -- avoid secondary load path;
2010-10-24 nipkow 2010-10-24 nat_number -> eval_nat_numeral
2010-05-20 haftmann 2010-05-20 renamed List_Set to the now more appropriate More_Set
2010-03-01 haftmann 2010-03-01 replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2010-02-11 wenzelm 2010-02-11 modernized translations;
2009-11-24 haftmann 2009-11-24 backported parts of abstract byte code verifier from AFP/Jinja
2009-07-14 haftmann 2009-07-14 code attributes use common underscore convention
2009-06-29 haftmann 2009-06-29 tuned
2009-06-29 haftmann 2009-06-29 explicit Set constructor for code generated for sets
2009-05-18 nipkow 2009-05-18 fine-tuned elimination of comprehensions involving x=t.
2009-05-16 nipkow 2009-05-16 proof tuned
2009-05-16 nipkow 2009-05-16 "{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}" by the new simproc defColl_regroup. More precisely, the simproc pulls an equation x=t (or t=x) out of a nest of conjunctions to the front where the simp rule singleton_conj_conv(2) converts to "if".
2008-10-07 haftmann 2008-10-07 tuned code setup
2007-08-20 wenzelm 2007-08-20 theory header: fixed import;
2007-08-20 wenzelm 2007-08-20 theory header: more precise imports;
2007-07-19 haftmann 2007-07-19 uniform naming conventions for CG theories
2007-07-11 berghofe 2007-07-11 - Renamed inductive2 to inductive - Renamed some theorems about transitive closure for predicates
2007-05-19 haftmann 2007-05-19 added qualification for ambiguous definition names
2007-02-07 berghofe 2007-02-07 Adapted to new inductive definition package.
2006-10-31 haftmann 2006-10-31 adapted to new serializer syntax
2006-10-10 haftmann 2006-10-10 removed quote in serialization
2006-09-19 haftmann 2006-09-19 added some stuff for code generation 2
2005-09-25 berghofe 2005-09-25 Now uses set implementation from ExecutableSet.
2005-09-17 wenzelm 2005-09-17 removed obsolete BasisLibrary;
2005-08-25 berghofe 2005-08-25 Adapted to new code generator syntax.
2005-07-01 berghofe 2005-07-01 Added BasisLibrary prefix to List.concat to avoid problems with modular code generation.
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2004-07-15 nipkow 2004-07-15 Moved to new m<..<n syntax for set intervals.
2003-05-26 streckem 2003-05-26 Introduced distinction wf_prog vs. ws_prog
2002-11-27 berghofe 2002-11-27 Fixed bug in consts_code section.
2002-06-14 kleing 2002-06-14 wt_method now checks bounded+types ==> wt_kildall <=> wt_method
2002-05-30 nipkow 2002-05-30 Modifications due to enhanced linear arithmetic.
2002-05-14 kleing 2002-05-14 numerals work again
2002-05-11 kleing 2002-05-11 fix for change in nat number simplification
2002-04-30 kleing 2002-04-30 tuned
2002-04-19 berghofe 2002-04-19 Added example for code generation.
2002-03-09 kleing 2002-03-09 canonical start state
2002-03-07 wenzelm 2002-03-07 renamed nat_number_of to nat_number (avoid clash with separate theorem);
2002-03-03 kleing 2002-03-03 symbolized
2002-02-28 kleing 2002-02-28 fixed document
2002-02-26 kleing 2002-02-26 introduces SystemClasses and BVExample