# HG changeset patch
# User wenzelm
# Date 971905492 -7200
# Node ID 41f6be79b44f6d1b28ca8f8ad235e9ec108a3d52
# Parent  4e004b548049ba172c1004b59848b7b062cff2b6
removed Library/Accessible_Part.ML;

diff -r 4e004b548049 -r 41f6be79b44f src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Oct 18 23:42:18 2000 +0200
+++ b/src/HOL/IsaMakefile	Wed Oct 18 23:44:52 2000 +0200
@@ -161,10 +161,10 @@
 
 HOL-Library: HOL $(LOG)/HOL-Library.gz
 
-$(LOG)/HOL-Library.gz: $(OUT)/HOL Library/Accessible_Part.ML \
-  Library/Accessible_Part.thy Library/Library.thy Library/Multiset.thy \
-  Library/Quotient.thy Library/README.html Library/ROOT.ML \
-  Library/While_Combinator.thy Library/While_Combinator_Example.thy
+$(LOG)/HOL-Library.gz: $(OUT)/HOL Library/Accessible_Part.thy \
+  Library/Library.thy Library/Multiset.thy Library/Quotient.thy \
+  Library/README.html Library/ROOT.ML Library/While_Combinator.thy \
+  Library/While_Combinator_Example.thy
 	@$(ISATOOL) usedir $(OUT)/HOL Library
 
 
diff -r 4e004b548049 -r 41f6be79b44f src/HOL/Library/Accessible_Part.ML
--- 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";