src/HOL/ex/Recdef.thy
changeset 3912 4ed64ad7fb42
parent 3842 b55686a7b22c
child 4100 9f6907c40442
equal deleted inserted replaced
3911:0165b805fe09 3912:4ed64ad7fb42