src/HOL/ex/ReflectionEx.thy
2010-12-29 wenzelm 2010-12-29 explicit file specifications -- avoid secondary load path;
2010-09-08 haftmann 2010-09-08 modernized primrec
2010-03-01 krauss 2010-03-01 more recdef (and old primrec) hunting
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-04-29 haftmann 2009-04-29 farewell to class recpower
2009-01-28 nipkow 2009-01-28 merged - resolving conflics
2009-01-28 nipkow 2009-01-28 Replaced group_ and ring_simps by algebra_simps; removed compare_rls - use algebra_simps now
2009-01-28 haftmann 2009-01-28 Reflection.thy now in HOL/Library
2008-11-20 wenzelm 2008-11-20 reactivated some dead theories (based on hints by Mark Hillebrand);
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).