src/HOL/Library/old_recdef.ML
Thu, 09 Jul 2015 15:20:54 +0200 wenzelm clarified context;
Sun, 05 Jul 2015 15:02:30 +0200 wenzelm simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
Fri, 19 Jun 2015 20:43:34 +0200 wenzelm removed dead code;
Fri, 19 Jun 2015 20:14:50 +0200 wenzelm discontinued unused 'defer_recdef';
Fri, 19 Jun 2015 19:45:01 +0200 wenzelm tuned;
Fri, 19 Jun 2015 19:29:57 +0200 wenzelm removed dead code;
Fri, 19 Jun 2015 19:13:15 +0200 wenzelm moved sources;
less more (0) tip