| Tue, 02 Aug 2011 08:28:34 -0700 | huffman | Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names | changeset | files |
| Tue, 02 Aug 2011 07:36:58 -0700 | huffman | NEWS: fix typo | changeset | files |
| Tue, 02 Aug 2011 13:07:00 +0200 | krauss | updated unchecked forward reference | changeset | files |
| Tue, 02 Aug 2011 12:27:24 +0200 | krauss | replaced Nitpick's hardwired basic_ersatz_table by context data | changeset | files |
| Tue, 02 Aug 2011 12:17:48 +0200 | krauss | NEWS | changeset | files |
| 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 |