src/HOL/Library/FinFun_Syntax.thy
changeset 53730 f2f6874893df
parent 51542 738598beeb26
child 58881 b9556a055632