author | wenzelm |
Wed, 18 Oct 2000 23:40:17 +0200 | |
changeset 10261 | bb2f1e859177 |
parent 10212 | 33fe2d701ddd |
child 10519 | ade64af4c57c |
permissions | -rw-r--r-- |
(* Title: HOL/List.thy ID: $Id$ Author: Tobias Nipkow 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 = Option + Wellfounded_Relations + NatSimprocs + Recdef + Record + Relation_Power + Calculation + SVC_Oracle: (*belongs to theory HOL*) declare case_split [cases type: bool] (*belongs to theory Wellfounded_Recursion*) declare wf_induct [induct set: wf] end