author | nipkow |
Fri, 04 Feb 2005 17:14:42 +0100 | |
changeset 15497 | 53bca254719a |
parent 15298 | a5bea99352d6 |
child 16760 | 5c5f051aaaaa |
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 imports Wellfounded_Relations Presburger Recdef Relation_Power Parity begin 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