src/HOL/ex/reflection_data.ML
2008-01-26 wenzelm 2008-01-26 tuned attribute syntax -- no need for eta-expansion;
2007-07-29 wenzelm 2007-07-29 renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms; tuned;
2007-07-08 chaieb 2007-07-08 Context data now consist of eqations for reification and equations for correctness theorems for reflection; Added attribute reflection to store correctness theorems to be trued by default
2007-07-06 chaieb 2007-07-06 Cleaned add and del attributes
2007-07-03 chaieb 2007-07-03 Context Data for the reflection and reification methods