src/HOL/Library/reflection.ML
2012-03-02 haftmann 2012-03-02 dropped dead code
2012-02-16 wenzelm 2012-02-16 more antiquotations;
2011-11-08 wenzelm 2011-11-08 tuned;
2011-07-25 bulwahn 2011-07-25 replacing conversion function of old code generator by the current code generator in the reflection tactic
2011-07-25 bulwahn 2011-07-25 fixed typo
2011-06-09 wenzelm 2011-06-09 renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
2011-04-20 wenzelm 2011-04-20 explicit context for Codegen.eval_term etc.;
2011-04-16 wenzelm 2011-04-16 proper subgoal addressing via SUBGOAL/CSUBGOAL -- assuming these tactics did not handle Subscript in any special way; tuned;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-08 wenzelm 2011-04-08 explicit structure Syntax_Trans; discontinued old-style constrainAbsC;
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-08-19 haftmann 2010-08-19 use antiquotations for remaining unqualified constants in HOL
2010-05-25 wenzelm 2010-05-25 eliminated various catch-all exception patterns, guessing at the concrete exeptions that are intended here;
2010-05-15 wenzelm 2010-05-15 less pervasive names from structure Thm;
2010-05-05 haftmann 2010-05-05 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 wenzelm 2010-03-07 modernized structure Local_Defs;
2009-10-17 wenzelm 2009-10-17 tuned/moved divide_and_conquer';
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-07-23 wenzelm 2009-07-23 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
2009-07-17 wenzelm 2009-07-17 tuned/modernized Envir.subst_XXX;
2009-07-17 wenzelm 2009-07-17 tuned/modernized Envir operations;
2009-07-10 haftmann 2009-07-10 dropped find_index_eq
2009-06-08 hoelzl 2009-06-08 Added new evaluator "approximate"
2009-06-24 wenzelm 2009-06-24 renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported); renamed Variable.importT_thms to Variable.importT (again);
2009-06-03 hoelzl 2009-06-03 Converted reification to use fold_map instead of Library.foldl_map. Use antiquotations.
2009-06-03 hoelzl 2009-06-03 Removed usage of reference in reification
2009-06-02 hoelzl 2009-06-02 corrected spacing in reflection
2009-04-24 haftmann 2009-04-24 added helpless comment
2009-03-27 haftmann 2009-03-27 dropped infix union
2009-02-27 wenzelm 2009-02-27 eliminated private clones of List.partition;
2009-02-09 hoelzl 2009-02-09 Proof method 'reify' is now reentrant.
2009-02-05 hoelzl 2009-02-05 Add approximation method
2009-01-28 haftmann 2009-01-28 Reflection.thy now in HOL/Library