src/HOL/Tools/recdef.ML
changeset 40407 2ff10e613689
parent 39557 fe5722fce758
child 42361 23f352990944
equal deleted inserted replaced
40406:313a24b66a8d 40407:2ff10e613689