removed Library/Accessible_Part.ML;
authorwenzelm
Wed Oct 18 23:44:52 2000 +0200 (2000-10-18)
changeset 1026641f6be79b44f
parent 10265 4e004b548049
child 10267 325ead6d9457
removed Library/Accessible_Part.ML;
src/HOL/IsaMakefile
src/HOL/Library/Accessible_Part.ML
     1.1 --- a/src/HOL/IsaMakefile	Wed Oct 18 23:42:18 2000 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Wed Oct 18 23:44:52 2000 +0200
     1.3 @@ -161,10 +161,10 @@
     1.4  
     1.5  HOL-Library: HOL $(LOG)/HOL-Library.gz
     1.6  
     1.7 -$(LOG)/HOL-Library.gz: $(OUT)/HOL Library/Accessible_Part.ML \
     1.8 -  Library/Accessible_Part.thy Library/Library.thy Library/Multiset.thy \
     1.9 -  Library/Quotient.thy Library/README.html Library/ROOT.ML \
    1.10 -  Library/While_Combinator.thy Library/While_Combinator_Example.thy
    1.11 +$(LOG)/HOL-Library.gz: $(OUT)/HOL Library/Accessible_Part.thy \
    1.12 +  Library/Library.thy Library/Multiset.thy Library/Quotient.thy \
    1.13 +  Library/README.html Library/ROOT.ML Library/While_Combinator.thy \
    1.14 +  Library/While_Combinator_Example.thy
    1.15  	@$(ISATOOL) usedir $(OUT)/HOL Library
    1.16  
    1.17  
     2.1 --- a/src/HOL/Library/Accessible_Part.ML	Wed Oct 18 23:42:18 2000 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,8 +0,0 @@
     2.4 -
     2.5 -val accI = thm "acc.accI";
     2.6 -val acc_induct = thm "acc_induct";
     2.7 -val acc_downward = thm "acc_downward";
     2.8 -val acc_downwards = thm "acc_downwards";
     2.9 -val acc_wfI = thm "acc_wfI";
    2.10 -val acc_wfD = thm "acc_wfD";
    2.11 -val wf_acc_iff = thm "wf_acc_iff";