src/HOL/Tools/old_primrec.ML
changeset 39371 6549ca3671f3
parent 36692 54b64d4ad524
child 39557 fe5722fce758
equal deleted inserted replaced
39370:f8292d3020db 39371:6549ca3671f3