src/HOL/Tools/recdef.ML
changeset 41373 48503e4e96b6
parent 39557 fe5722fce758
child 42361 23f352990944
equal deleted inserted replaced
41372:551eb49a6e91 41373:48503e4e96b6