src/HOL/PreList.thy
author paulson
Thu Mar 04 12:06:07 2004 +0100 (2004-03-04)
changeset 14430 5cb24165a2e1
parent 14125 bf8edef6c1f1
child 14577 dbb95b825244
permissions -rw-r--r--
new material from Avigad, and simplified treatment of division by 0
     1 (*  Title:      HOL/PreList.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow and Markus Wenzel
     4     Copyright   2000 TU Muenchen
     5 *)
     6 
     7 header{*A Basis for Building the Theory of Lists*}
     8 
     9 (*Is defined separately to serve as a basis for theory ToyList in the
    10 documentation.*)
    11 
    12 theory PreList =
    13     Wellfounded_Relations + Presburger + Recdef + Relation_Power + Parity:
    14 
    15 (*belongs to theory Wellfounded_Recursion*)
    16 lemmas wf_induct_rule = wf_induct [rule_format, case_names less, induct set: wf]
    17 
    18 end