src/HOL/Tools/inductive_package.ML
changeset 25571 c9e39eafc7a0
parent 25510 38c15efe603b
child 25822 05756950011c
equal deleted inserted replaced
25570:fdfbbb92dadf 25571:c9e39eafc7a0