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 |
Tue, 02 Aug 2011 10:36:50 +0200 | krauss | moved recdef package to HOL/Library/Old_Recdef.thy | file | diff | annotate | base |