src/HOL/BNF_Def.thy
changeset 60243 5901cb4db0ae
parent 59726 64c2bb331035
child 60758 d8d85a8172b5