src/HOL/Recdef.thy
changeset 27107 4a7415c67063
parent 26748 4d51ddd6aa5c
child 29654 24e73987bfe2
equal deleted inserted replaced
27106:ff27dc6e7d05 27107:4a7415c67063