src/HOL/PreList.thy
changeset 10733 59f82484e000
parent 10680 26e4aecf3207
child 11787 85b3735a51e1
equal deleted inserted replaced
10732:d4fda7d05ce5 10733:59f82484e000
     1 (*  Title:      HOL/PreList.thy
     1 (*  Title:      HOL/PreList.thy
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     3     Author:     Tobias Nipkow and Markus Wenzel
     4     Copyright   2000 TU Muenchen
     4     Copyright   2000 TU Muenchen
     5 
     5 
     6 A basis for building theory List on. Is defined separately to serve as a
     6 A basis for building theory List on. Is defined separately to serve as a
     7 basis for theory ToyList in the documentation.
     7 basis for theory ToyList in the documentation.
     8 *)
     8 *)
    17 (*belongs to theory Wellfounded_Recursion*)
    17 (*belongs to theory Wellfounded_Recursion*)
    18 declare wf_induct [induct set: wf]
    18 declare wf_induct [induct set: wf]
    19 
    19 
    20 (*belongs to theory Datatype_Universe; hides popular names *)
    20 (*belongs to theory Datatype_Universe; hides popular names *)
    21 hide const Node Atom Leaf Numb Lim Funs Split Case
    21 hide const Node Atom Leaf Numb Lim Funs Split Case
       
    22 hide type node item
    22 
    23 
    23 
    24 
    24 (* generic summation indexed over nat *)
    25 (* generic summation indexed over nat *)
    25 
    26 
    26 (*FIXME move to Ring_and_Field, when it is made part of main HOL (!?)*)
    27 (*FIXME move to Ring_and_Field, when it is made part of main HOL (!?)*)