src/HOL/Library/FinFun_Syntax.thy
changeset 63127 360d9997fac9
parent 62390 842917225d56