src/HOL/BNF_Def.thy
changeset 60048 e9c30726ca8e
parent 59726 64c2bb331035
child 60758 d8d85a8172b5