src/HOL/Library/FinFun_Syntax.thy
changeset 60806 622d45ca75ee
parent 60500 903bb1495239
child 61384 9f5145281888
equal deleted inserted replaced
60804:080a979a985b 60806:622d45ca75ee