author | berghofe |
Tue, 25 Mar 2003 09:49:13 +0100 | |
changeset 13878 | 90ca3815e4b2 |
parent 13877 | a6b825ee48d9 |
child 13879 | 92c0973ac730 |
--- a/src/HOL/PreList.thy Tue Mar 25 09:48:38 2003 +0100 +++ b/src/HOL/PreList.thy Tue Mar 25 09:49:13 2003 +0100 @@ -8,7 +8,7 @@ *) theory PreList = - Wellfounded_Relations + NatSimprocs + Recdef + Relation_Power: + Wellfounded_Relations + Presburger + Recdef + Relation_Power: (*belongs to theory Divides*) declare dvdI [intro?] dvdE [elim?] dvd_trans [trans]