src/HOL/Recdef.thy
changeset 11944 0594e63e6057
parent 11533 0c0d2332e8f0
child 12023 d982f98e0f0d
equal deleted inserted replaced
11943:a9672446b45f 11944:0594e63e6057