author berghofe
Tue, 25 Mar 2003 09:49:13 +0100
changeset 13878 90ca3815e4b2
parent 13297 e4ae0732e2be
child 14125 bf8edef6c1f1
permissions -rw-r--r--
Added Presburger theory.

(*  Title:      HOL/PreList.thy
    ID:         $Id$
    Author:     Tobias Nipkow and Markus Wenzel
    Copyright   2000 TU Muenchen

A basis for building theory List on. Is defined separately to serve as a
basis for theory ToyList in the documentation.

theory PreList =
  Wellfounded_Relations + Presburger + Recdef + Relation_Power:

(*belongs to theory Divides*)
declare dvdI [intro?]  dvdE [elim?]  dvd_trans [trans]

(*belongs to theory Nat*)
lemmas less_induct = nat_less_induct [rule_format, case_names less]

(*belongs to theory Wellfounded_Recursion*)
lemmas wf_induct_rule = wf_induct [rule_format, case_names less, induct set: wf]