src/HOL/BNF_Def.thy
changeset 58710 7216a10d69ba
parent 58446 e89f57d1e46c
child 58889 5b7a9633cfa8