# HG changeset patch # User berghofe # Date 1048582153 -3600 # Node ID 90ca3815e4b296d1279b1316dee78431599313e6 # Parent a6b825ee48d9a34a3021bbe4be6157f144c4fa03 Added Presburger theory. diff -r a6b825ee48d9 -r 90ca3815e4b2 src/HOL/PreList.thy --- 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]