src/HOL/ex/ReflectionEx.thy
Wed, 29 Dec 2010 17:34:41 +0100 wenzelm explicit file specifications -- avoid secondary load path;
Wed, 08 Sep 2010 19:21:46 +0200 haftmann modernized primrec
Mon, 01 Mar 2010 17:05:57 +0100 krauss more recdef (and old primrec) hunting
Fri, 05 Feb 2010 14:33:50 +0100 haftmann more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
Sat, 17 Oct 2009 14:43:18 +0200 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
Wed, 29 Apr 2009 14:20:26 +0200 haftmann farewell to class recpower
Wed, 28 Jan 2009 16:57:12 +0100 nipkow merged - resolving conflics
Wed, 28 Jan 2009 16:29:16 +0100 nipkow Replaced group_ and ring_simps by algebra_simps;
Wed, 28 Jan 2009 11:04:10 +0100 haftmann Reflection.thy now in HOL/Library
Thu, 20 Nov 2008 19:43:34 +0100 wenzelm reactivated some dead theories (based on hints by Mark Hillebrand);
Sun, 08 Jul 2007 19:01:32 +0200 chaieb Show the use of reflection attribute; fixed comments about the order of absorbing equations : f (C x) = x ; now automaically tried as last;
Sat, 07 Jul 2007 11:09:40 +0200 chaieb The order for parameter for interpretation is now inversted:
Fri, 06 Jul 2007 16:09:28 +0200 chaieb Some examples for reifying type variables
Tue, 03 Jul 2007 17:49:58 +0200 chaieb More examples
Sat, 23 Jun 2007 19:33:22 +0200 nipkow tuned and renamed group_eq_simps and ring_eq_simps
less more (0) -15 tip