src/HOL/Library/FinFun_Syntax.thy
changeset 58256 08c0f0d4b9f4
parent 51542 738598beeb26
child 58881 b9556a055632