src/HOL/ex/ReflectionEx.thy
2007-07-08 chaieb 2007-07-08 Show the use of reflection attribute; fixed comments about the order of absorbing equations : f (C x) = x ; now automaically tried as last;
2007-07-07 chaieb 2007-07-07 The order for parameter for interpretation is now inversted: f t env0 env1 ... envn = ... where t is the type to be reified;
2007-07-06 chaieb 2007-07-06 Some examples for reifying type variables
2007-07-03 chaieb 2007-07-03 More examples
2007-06-23 nipkow 2007-06-23 tuned and renamed group_eq_simps and ring_eq_simps
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-09-18 chaieb 2006-09-18 Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n) instead of only ... = xs!n.
2006-09-11 wenzelm 2006-09-11 induct method: renamed 'fixing' to 'arbitrary';
2006-08-14 chaieb 2006-08-14 Reification now handels binders.
2006-08-04 chaieb 2006-08-04 *** empty log message ***
2006-08-03 wenzelm 2006-08-03 Generic reflection and reification (by Amine Chaieb).