src/HOL/Library/Accessible_Part.ML
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";