src/HOL/MicroJava/Comp/LemmasComp.thy
2014-09-04 hoelzl 2014-09-04 cleanup Wfrec; introduce dependent_wf/wellorder_choice
2014-03-15 haftmann 2014-03-15 more complete set of lemmas wrt. image and composition
2014-02-16 blanchet 2014-02-16 folded 'list_all2' with the relator generated by 'datatype_new'
2014-02-14 blanchet 2014-02-14 merged 'Option.map' and 'Option.map_option'
2013-08-02 wenzelm 2013-08-02 tuned proofs;
2012-07-27 wenzelm 2012-07-27 tuned proofs -- avoid odd situations of polymorphic Frees in goal state;
2012-01-15 wenzelm 2012-01-15 tuned proofs;
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-03-06 haftmann 2010-03-06 "private" map_of_map lemma
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-11-12 hoelzl 2009-11-12 Remove map_compose, replaced by map_map
2009-11-12 hoelzl 2009-11-12 New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-03-04 nipkow 2009-03-04 Made Option a separate theory and renamed option_map to Option.map
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.
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-06-16 paulson 2004-06-16 removal of x-symbol syntax <Sigma> for dependent products
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-10-23 streckem 2002-10-23 First checkin of compiler