src/HOL/Recdef.thy
changeset 39560 c13b4589fddf
parent 39302 d7728f65b353
equal deleted inserted replaced
39551:92a6ec7464e4 39560:c13b4589fddf