src/HOL/Tools/recdef.ML
changeset 63673 2314e99c18a7
parent 60520 09fc5eaa21ce
equal deleted inserted replaced
63672:5a7c919a4ada 63673:2314e99c18a7