src/HOL/BNF_Def.thy
changeset 58151 414deb2ef328
parent 58106 c8cba801c483
child 58352 37745650a3f4