author | wenzelm |
Sat, 05 Jun 2004 13:07:04 +0200 | |
changeset 14872 | 3f2144aebd76 |
parent 14577 | dbb95b825244 |
child 15131 | c69542757a4d |
permissions | -rw-r--r-- |
(* Title: HOL/PreList.thy ID: $Id$ Author: Tobias Nipkow and Markus Wenzel Copyright 2000 TU Muenchen *) header{*A Basis for Building the Theory of Lists*} theory PreList = Wellfounded_Relations + Presburger + Recdef + Relation_Power + Parity: text {* Is defined separately to serve as a basis for theory ToyList in the documentation. *} lemmas wf_induct_rule = wf_induct [rule_format, case_names less, induct set: wf] -- {* belongs to theory @{text Wellfounded_Recursion} *} end