src/HOL/Tools/recdef.ML
changeset 33670 02b7738aef6a
parent 33643 b275f26a638b
child 33699 f33b036ef318
equal deleted inserted replaced
33669:ae9a2ea9a989 33670:02b7738aef6a