src/HOL/Main.thy
author nipkow
Fri Nov 24 16:49:27 2000 +0100 (2000-11-24)
changeset 10519 ade64af4c57c
parent 10386 581a5a143994
child 11483 f4d10044a2cd
permissions -rw-r--r--
hide many names from Datatype_Universe.
     1 (*  Title:      HOL/Main.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   2000 TU Muenchen
     5 
     6 Theory Main includes everything.
     7 Note that theory PreList already includes most HOL theories.
     8 *)
     9 
    10 theory Main = Map + String:
    11 
    12 (*belongs to theory List*)
    13 declare lists_mono [mono]
    14 declare map_cong [recdef_cong]
    15 lemmas rev_induct [case_names Nil snoc] = rev_induct
    16   and rev_cases [case_names Nil snoc] = rev_exhaust
    17 
    18 end