src/HOL/PreList.thy
author wenzelm
Thu Jul 04 16:48:21 2002 +0200 (2002-07-04)
changeset 13297 e4ae0732e2be
parent 12919 d6a0d168291e
child 13878 90ca3815e4b2
permissions -rw-r--r--
tuned;
     1 (*  Title:      HOL/PreList.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow and Markus Wenzel
     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 *)
     9 
    10 theory PreList =
    11   Wellfounded_Relations + NatSimprocs + Recdef + Relation_Power:
    12 
    13 (*belongs to theory Divides*)
    14 declare dvdI [intro?]  dvdE [elim?]  dvd_trans [trans]
    15 
    16 (*belongs to theory Nat*)
    17 lemmas less_induct = nat_less_induct [rule_format, case_names less]
    18 
    19 (*belongs to theory Wellfounded_Recursion*)
    20 lemmas wf_induct_rule = wf_induct [rule_format, case_names less, induct set: wf]
    21 
    22 end