src/HOL/ex/Execute_Choice.thy
2012-10-18 kuncar 2012-10-18 update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
2011-09-12 bulwahn 2011-09-12 correcting imports after splitting and renaming AssocList
2011-08-12 huffman 2011-08-12 make more HOL theories work with separate set type
2010-12-29 wenzelm 2010-12-29 explicit file specifications -- avoid secondary load path;
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-06-28 haftmann 2010-06-28 dropped ancient infix mem; refined code generation operations in List.thy
2010-05-21 haftmann 2010-05-21 adjusted to changes in Mapping.thy
2010-04-11 haftmann 2010-04-11 constructor Mapping replaces AList
2010-02-17 haftmann 2010-02-17 example for executable choice
2010-02-17 haftmann 2010-02-17 a draft for an example how to turn specifications involving choice executable