src/HOL/Library/Accessible_Part.ML

The accessible part of a relation (from HOL/Induct/Acc);

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";