author | nipkow |
Thu, 12 Oct 2000 13:01:19 +0200 | |
changeset 10202 | 9e8b4bebc940 |
parent 9619 | 6125cc9efc18 |
child 10212 | 33fe2d701ddd |
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 + WF_Rel + NatSimprocs + Recdef + Record + RelPow + Calculation + SVC_Oracle + While: theorems [cases type: bool] = case_split end