src/HOL/Wfrec.thy
2014-01-16 blanchet 2014-01-16 adapted to move of Wfrec
2014-01-16 blanchet 2014-01-16 moved Wfrec to Main, since it is a dependency of cardinals, hence BNFs