src/HOL/ex/Reflection.thy
2007-07-08 chaieb 2007-07-08 Changed syntax for the reflection method (reify unchanged). reflection takes an optional set of theorems for reification then several correctness theorems are specified by rules:'' then the optional term is specified by only:
2007-07-06 chaieb 2007-07-06 Tuned document
2007-07-03 chaieb 2007-07-03 reflection and reification methods now manage Context data
2007-01-28 chaieb 2007-01-28 Now deals with simples cases where the input equations contain type variables See example in ReflectionEx.thy
2006-12-18 haftmann 2006-12-18 switched argument order in *.syntax lifters
2006-11-29 wenzelm 2006-11-29 simplified method setup;
2006-08-14 chaieb 2006-08-14 Reification now handels binders.
2006-08-03 wenzelm 2006-08-03 Generic reflection and reification (by Amine Chaieb).