changeset 10266 | 41f6be79b44f |
parent 10265 | 4e004b548049 |
child 10267 | 325ead6d9457 |
--- a/src/HOL/Library/Accessible_Part.ML Wed Oct 18 23:42:18 2000 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,8 +0,0 @@ - -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";