src/HOL/Main.thy
author oheimb
Wed Jan 31 10:15:55 2001 +0100 (2001-01-31)
changeset 11008 f7333f055ef6
parent 10519 ade64af4c57c
child 11483 f4d10044a2cd
permissions -rw-r--r--
improved theory reference in comment
     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