| Tue, 02 Aug 2011 11:52:57 +0200 | krauss | moved recursion combinator to HOL/Library/Wfrec.thy -- it is so fundamental and well-known that it should survive recdef | changeset | files |
| Tue, 02 Aug 2011 10:36:50 +0200 | krauss | moved recdef package to HOL/Library/Old_Recdef.thy | changeset | files |
| Tue, 02 Aug 2011 10:03:14 +0200 | krauss | added dynamic ersatz_table to Nitpick's data slot | changeset | files |