rec_def.thy
changeset 41 6d89ed67ba27
parent 0 aa8656a8dbef