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
nipkow@10519
     1
(*  Title:      HOL/PreList.thy
nipkow@8563
     2
    ID:         $Id$
wenzelm@10733
     3
    Author:     Tobias Nipkow and Markus Wenzel
nipkow@8563
     4
    Copyright   2000 TU Muenchen
nipkow@8563
     5
*)
wenzelm@8490
     6
paulson@14125
     7
header{*A Basis for Building the Theory of Lists*}
wenzelm@12020
     8
paulson@14125
     9
(*Is defined separately to serve as a basis for theory ToyList in the
paulson@14125
    10
documentation.*)
wenzelm@8490
    11
paulson@14430
    12
theory PreList =
paulson@14430
    13
    Wellfounded_Relations + Presburger + Recdef + Relation_Power + Parity:
wenzelm@12397
    14
wenzelm@10261
    15
(*belongs to theory Wellfounded_Recursion*)
wenzelm@12397
    16
lemmas wf_induct_rule = wf_induct [rule_format, case_names less, induct set: wf]
wenzelm@9066
    17
wenzelm@8490
    18
end