src/HOL/PreList.thy
author wenzelm
Wed Jun 14 17:59:53 2000 +0200 (2000-06-14)
changeset 9066 b1e874e38dab
parent 8862 78643f8449c6
child 9619 6125cc9efc18
permissions -rw-r--r--
theorems [cases type: bool] = case_split;
     1 (*  Title:      HOL/List.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   2000 TU Muenchen
     5 
     6 A basis for building theory List on. Is defined separately to serve as a
     7 basis for theory ToyList in the documentation.
     8 *)
     9 
    10 theory PreList =
    11   Option + WF_Rel + NatSimprocs + Recdef + Record + RelPow + Calculation + 
    12   SVC_Oracle:
    13 
    14 theorems [cases type: bool] = case_split
    15 
    16 end