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