src/HOL/Tools/recdef_package.ML
changeset 27982 2aaa4a5569a6
parent 27809 a1e409db516b
child 28083 103d9282a946
equal deleted inserted replaced
27981:feb0c01cf0fb 27982:2aaa4a5569a6