src/HOL/BNF_Def.thy
changeset 56524 f4ba736040fa
parent 55945 e96383acecf9
child 56635 b07c8ad23010