| Wed, 17 Aug 2011 14:42:59 -0700 | huffman | Wfrec.thy: respect set/pred distinction | file | diff | annotate |
| 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 | file | diff | annotate |