src/HOL/Wellfounded_Recursion.thy
changeset 15977 aa6744dd998e
parent 15950 5c067c956a20
child 17042 da5cfaa258f7