src/HOL/Recdef.thy
changeset 15283 f21466450330
parent 15150 c7af682b9ee5
child 15481 fc075ae929e4
equal deleted inserted replaced
15282:765d5d6e4468 15283:f21466450330