# HG changeset patch
# User paulson
# Date 1059057351 -7200
# Node ID bf8edef6c1f1be9bbb719ce4b970cb2a6523ce15
# Parent  883c38e2d4c0ce6b481a6a2c12d3b34f460e3a04
tidied

diff -r 883c38e2d4c0 -r bf8edef6c1f1 src/HOL/PreList.thy
--- a/src/HOL/PreList.thy	Tue Jul 22 11:05:02 2003 +0200
+++ b/src/HOL/PreList.thy	Thu Jul 24 16:35:51 2003 +0200
@@ -2,19 +2,14 @@
     ID:         $Id$
     Author:     Tobias Nipkow and Markus Wenzel
     Copyright   2000 TU Muenchen
-
-A basis for building theory List on. Is defined separately to serve as a
-basis for theory ToyList in the documentation.
 *)
 
-theory PreList =
-  Wellfounded_Relations + Presburger + Recdef + Relation_Power:
+header{*A Basis for Building the Theory of Lists*}
 
-(*belongs to theory Divides*)
-declare dvdI [intro?]  dvdE [elim?]  dvd_trans [trans]
+(*Is defined separately to serve as a basis for theory ToyList in the
+documentation.*)
 
-(*belongs to theory Nat*)
-lemmas less_induct = nat_less_induct [rule_format, case_names less]
+theory PreList = Wellfounded_Relations + Presburger + Recdef + Relation_Power:
 
 (*belongs to theory Wellfounded_Recursion*)
 lemmas wf_induct_rule = wf_induct [rule_format, case_names less, induct set: wf]