| changeset 12304 | 8df202daf55d |
| parent 12020 | a24373086908 |
| child 12397 | 6766aa05e4eb |
--- a/src/HOL/PreList.thy Wed Nov 28 00:37:08 2001 +0100 +++ b/src/HOL/PreList.thy Wed Nov 28 00:37:40 2001 +0100 @@ -12,7 +12,7 @@ Relation_Power + SVC_Oracle: (*belongs to theory Divides*) -declare dvd_trans [trans] +declare dvdI [intro?] dvdE [elim?] dvd_trans [trans] (*belongs to theory Wellfounded_Recursion*) declare wf_induct [induct set: wf]