src/HOL/Recdef.thy
changeset 30005 7d97e20728d4
parent 29654 24e73987bfe2
child 31723 f5cafe803b55
equal deleted inserted replaced
30001:dd27e16677b2 30005:7d97e20728d4