src/HOL/Recdef.thy
changeset 10840 28a53b68a8c0
parent 10773 0deff0197496
child 11165 3b69feb7d053
equal deleted inserted replaced
10839:1f93f5a27de6 10840:28a53b68a8c0