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.
nipkow@10519
     1
(*  Title:      HOL/PreList.thy
nipkow@8563
     2
    ID:         $Id$
nipkow@8563
     3
    Author:     Tobias Nipkow
nipkow@8563
     4
    Copyright   2000 TU Muenchen
nipkow@8563
     5
nipkow@8563
     6
A basis for building theory List on. Is defined separately to serve as a
nipkow@8563
     7
basis for theory ToyList in the documentation.
nipkow@8563
     8
*)
wenzelm@8490
     9
wenzelm@8490
    10
theory PreList =
nipkow@10212
    11
  Option + Wellfounded_Relations + NatSimprocs + Recdef + Record +
wenzelm@10261
    12
  Relation_Power + Calculation + SVC_Oracle:
wenzelm@8490
    13
wenzelm@10261
    14
(*belongs to theory HOL*)
wenzelm@10261
    15
declare case_split [cases type: bool]
wenzelm@10261
    16
wenzelm@10261
    17
(*belongs to theory Wellfounded_Recursion*)
wenzelm@10261
    18
declare wf_induct [induct set: wf]
wenzelm@9066
    19
nipkow@10519
    20
(*belongs to theory Datatype_Universe; hides popular names *)
nipkow@10519
    21
hide const Node Atom Leaf Numb Lim Funs Split Case
nipkow@10519
    22
wenzelm@8490
    23
end