src/HOL/Induct/Acc.ML
changeset 10258 d549f2534e6d
parent 10257 21055ac27708
child 10259 93ec82d535f2
     1.1 --- a/src/HOL/Induct/Acc.ML	Wed Oct 18 23:35:56 2000 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,8 +0,0 @@
     1.4 -
     1.5 -val accI = thm "acc.accI";
     1.6 -val acc_induct = thm "acc_induct";
     1.7 -val acc_downward = thm "acc_downward";
     1.8 -val acc_downwards = thm "acc_downwards";
     1.9 -val acc_wfI = thm "acc_wfI";
    1.10 -val acc_wfD = thm "acc_wfD";
    1.11 -val wf_acc_iff = thm "wf_acc_iff";