src/HOL/BNF_Def.thy
changeset 60609 15620ae824c0
parent 59726 64c2bb331035
child 60758 d8d85a8172b5