src/HOL/PreList.thy
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]