src/HOL/BNF_Def.thy
changeset 61597 53e32a9b66b8
parent 61424 c3658c18b7bc
child 61681 ca53150406c9