src/HOL/BNF_Def.thy
changeset 55400 1e8dd9cd320b
parent 55163 a740f312d9e4
child 55414 eab03e9cee8a