| changeset 15298 | a5bea99352d6 |
| parent 15231 | 96d5b6e2b6e4 |
| child 16760 | 5c5f051aaaaa |
--- a/src/HOL/PreList.thy Thu Nov 18 18:46:09 2004 +0100 +++ b/src/HOL/PreList.thy Fri Nov 19 14:00:31 2004 +0100 @@ -7,7 +7,7 @@ header{*A Basis for Building the Theory of Lists*} theory PreList -imports Wellfounded_Relations Barith Recdef Relation_Power Parity +imports Wellfounded_Relations Presburger Recdef Relation_Power Parity begin text {*