src/HOL/PreList.thy
changeset 14125 bf8edef6c1f1
parent 13878 90ca3815e4b2
child 14430 5cb24165a2e1
equal deleted inserted replaced
14124:883c38e2d4c0 14125:bf8edef6c1f1
     1 (*  Title:      HOL/PreList.thy
     1 (*  Title:      HOL/PreList.thy
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Tobias Nipkow and Markus Wenzel
     3     Author:     Tobias Nipkow and Markus Wenzel
     4     Copyright   2000 TU Muenchen
     4     Copyright   2000 TU Muenchen
     5 
       
     6 A basis for building theory List on. Is defined separately to serve as a
       
     7 basis for theory ToyList in the documentation.
       
     8 *)
     5 *)
     9 
     6 
    10 theory PreList =
     7 header{*A Basis for Building the Theory of Lists*}
    11   Wellfounded_Relations + Presburger + Recdef + Relation_Power:
       
    12 
     8 
    13 (*belongs to theory Divides*)
     9 (*Is defined separately to serve as a basis for theory ToyList in the
    14 declare dvdI [intro?]  dvdE [elim?]  dvd_trans [trans]
    10 documentation.*)
    15 
    11 
    16 (*belongs to theory Nat*)
    12 theory PreList = Wellfounded_Relations + Presburger + Recdef + Relation_Power:
    17 lemmas less_induct = nat_less_induct [rule_format, case_names less]
       
    18 
    13 
    19 (*belongs to theory Wellfounded_Recursion*)
    14 (*belongs to theory Wellfounded_Recursion*)
    20 lemmas wf_induct_rule = wf_induct [rule_format, case_names less, induct set: wf]
    15 lemmas wf_induct_rule = wf_induct [rule_format, case_names less, induct set: wf]
    21 
    16 
    22 end
    17 end