src/HOL/PreList.thy
author paulson
Thu Jul 24 16:35:51 2003 +0200 (2003-07-24)
changeset 14125 bf8edef6c1f1
parent 13878 90ca3815e4b2
child 14430 5cb24165a2e1
permissions -rw-r--r--
tidied
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@14125
    12
theory PreList = Wellfounded_Relations + Presburger + Recdef + Relation_Power:
wenzelm@12397
    13
wenzelm@10261
    14
(*belongs to theory Wellfounded_Recursion*)
wenzelm@12397
    15
lemmas wf_induct_rule = wf_induct [rule_format, case_names less, induct set: wf]
wenzelm@9066
    16
wenzelm@8490
    17
end