val accI = thm "acc.accI"; val acc_induct = thm "acc_induct"; val acc_downward = thm "acc_downward"; val acc_downwards = thm "acc_downwards"; val acc_wfI = thm "acc_wfI"; val acc_wfD = thm "acc_wfD"; val wf_acc_iff = thm "wf_acc_iff";