2010-05-05 ago farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
2010-03-07 ago modernized structure Local_Defs;
2009-10-17 ago tuned/moved divide_and_conquer';
2009-10-17 ago eliminated hard tabulators, guessing at each author's individual tab-width;
2009-07-23 ago renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
2009-07-17 ago tuned/modernized Envir.subst_XXX;
2009-07-17 ago tuned/modernized Envir operations;
2009-07-10 ago dropped find_index_eq
2009-06-08 ago Added new evaluator "approximate"
2009-06-24 ago renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
2009-06-03 ago Converted reification to use fold_map instead of Library.foldl_map. Use antiquotations.
2009-06-03 ago Removed usage of reference in reification
2009-06-02 ago corrected spacing in reflection
2009-04-24 ago added helpless comment
2009-03-27 ago dropped infix union
2009-02-27 ago eliminated private clones of List.partition;
2009-02-09 ago Proof method 'reify' is now reentrant.
2009-02-05 ago Add approximation method
2009-01-28 ago Reflection.thy now in HOL/Library