src/HOL/Recdef.thy
changeset 30929 d9343c0aac11
parent 29654 24e73987bfe2
child 31723 f5cafe803b55
equal deleted inserted replaced
30928:983dfcce45ad 30929:d9343c0aac11