nipkow@10519: (*  Title:      HOL/Main.thy
nipkow@10519:     ID:         $Id$
nipkow@10519:     Author:     Tobias Nipkow
nipkow@10519:     Copyright   2000 TU Muenchen
wenzelm@9619: 
nipkow@10519: Theory Main includes everything.
nipkow@10519: Note that theory PreList already includes most HOL theories.
nipkow@10519: *)
wenzelm@9619: 
wenzelm@9650: theory Main = Map + String:
wenzelm@9650: 
wenzelm@10261: (*belongs to theory List*)
wenzelm@10261: declare lists_mono [mono]
wenzelm@10261: declare map_cong [recdef_cong]
wenzelm@10386: lemmas rev_induct [case_names Nil snoc] = rev_induct
wenzelm@10386:   and rev_cases [case_names Nil snoc] = rev_exhaust
wenzelm@9768: 
wenzelm@9650: end