src/HOL/Library/bnf_lfp_countable.ML
changeset 59338 2ea1bf517842
parent 58634 9f10d82e8188
child 59498 50b60f501b05