src/HOL/Recdef.thy
changeset 39655 8ad7fe9d6f0b
parent 39302 d7728f65b353
equal deleted inserted replaced
39654:1207e39f0c7f 39655:8ad7fe9d6f0b