src/HOL/PreList.thy
author berghofe
Tue Mar 25 09:49:13 2003 +0100 (2003-03-25)
changeset 13878 90ca3815e4b2
parent 13297 e4ae0732e2be
child 14125 bf8edef6c1f1
permissions -rw-r--r--
Added Presburger theory.
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
nipkow@8563
     6
A basis for building theory List on. Is defined separately to serve as a
nipkow@8563
     7
basis for theory ToyList in the documentation.
nipkow@8563
     8
*)
wenzelm@8490
     9
wenzelm@8490
    10
theory PreList =
berghofe@13878
    11
  Wellfounded_Relations + Presburger + Recdef + Relation_Power:
wenzelm@12020
    12
wenzelm@12020
    13
(*belongs to theory Divides*)
wenzelm@12304
    14
declare dvdI [intro?]  dvdE [elim?]  dvd_trans [trans]
wenzelm@8490
    15
wenzelm@12397
    16
(*belongs to theory Nat*)
wenzelm@12397
    17
lemmas less_induct = nat_less_induct [rule_format, case_names less]
wenzelm@12397
    18
wenzelm@10261
    19
(*belongs to theory Wellfounded_Recursion*)
wenzelm@12397
    20
lemmas wf_induct_rule = wf_induct [rule_format, case_names less, induct set: wf]
wenzelm@9066
    21
wenzelm@8490
    22
end