author | schirmer |
Tue, 20 Jan 2004 13:56:27 +0100 | |
changeset 14359 | 3d9948163018 |
parent 14125 | bf8edef6c1f1 |
child 14430 | 5cb24165a2e1 |
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*} (*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 Wellfounded_Recursion*) lemmas wf_induct_rule = wf_induct [rule_format, case_names less, induct set: wf] end