src/HOL/PreList.thy
changeset 14125 bf8edef6c1f1
parent 13878 90ca3815e4b2
child 14430 5cb24165a2e1
     1.1 --- a/src/HOL/PreList.thy	Tue Jul 22 11:05:02 2003 +0200
     1.2 +++ b/src/HOL/PreList.thy	Thu Jul 24 16:35:51 2003 +0200
     1.3 @@ -2,19 +2,14 @@
     1.4      ID:         $Id$
     1.5      Author:     Tobias Nipkow and Markus Wenzel
     1.6      Copyright   2000 TU Muenchen
     1.7 -
     1.8 -A basis for building theory List on. Is defined separately to serve as a
     1.9 -basis for theory ToyList in the documentation.
    1.10  *)
    1.11  
    1.12 -theory PreList =
    1.13 -  Wellfounded_Relations + Presburger + Recdef + Relation_Power:
    1.14 +header{*A Basis for Building the Theory of Lists*}
    1.15  
    1.16 -(*belongs to theory Divides*)
    1.17 -declare dvdI [intro?]  dvdE [elim?]  dvd_trans [trans]
    1.18 +(*Is defined separately to serve as a basis for theory ToyList in the
    1.19 +documentation.*)
    1.20  
    1.21 -(*belongs to theory Nat*)
    1.22 -lemmas less_induct = nat_less_induct [rule_format, case_names less]
    1.23 +theory PreList = Wellfounded_Relations + Presburger + Recdef + Relation_Power:
    1.24  
    1.25  (*belongs to theory Wellfounded_Recursion*)
    1.26  lemmas wf_induct_rule = wf_induct [rule_format, case_names less, induct set: wf]