src/HOL/PreList.thy
author nipkow
Fri Nov 24 16:49:27 2000 +0100 (2000-11-24)
changeset 10519 ade64af4c57c
parent 10261 bb2f1e859177
child 10671 ac6b3b671198
permissions -rw-r--r--
hide many names from Datatype_Universe.
     1 (*  Title:      HOL/PreList.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 + Wellfounded_Relations + NatSimprocs + Recdef + Record +
    12   Relation_Power + Calculation + SVC_Oracle:
    13 
    14 (*belongs to theory HOL*)
    15 declare case_split [cases type: bool]
    16 
    17 (*belongs to theory Wellfounded_Recursion*)
    18 declare wf_induct [induct set: wf]
    19 
    20 (*belongs to theory Datatype_Universe; hides popular names *)
    21 hide const Node Atom Leaf Numb Lim Funs Split Case
    22 
    23 end