src/HOL/BNF_Def.thy
changeset 61841 4d3527b94f2a
parent 61681 ca53150406c9
child 62324 ae44f16dcea5