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.
nipkow@10519
     1
(*  Title:      HOL/Main.thy
nipkow@10519
     2
    ID:         $Id$
nipkow@10519
     3
    Author:     Tobias Nipkow
nipkow@10519
     4
    Copyright   2000 TU Muenchen
wenzelm@9619
     5
nipkow@10519
     6
Theory Main includes everything.
nipkow@10519
     7
Note that theory PreList already includes most HOL theories.
nipkow@10519
     8
*)
wenzelm@9619
     9
wenzelm@9650
    10
theory Main = Map + String:
wenzelm@9650
    11
wenzelm@10261
    12
(*belongs to theory List*)
wenzelm@10261
    13
declare lists_mono [mono]
wenzelm@10261
    14
declare map_cong [recdef_cong]
wenzelm@10386
    15
lemmas rev_induct [case_names Nil snoc] = rev_induct
wenzelm@10386
    16
  and rev_cases [case_names Nil snoc] = rev_exhaust
wenzelm@9768
    17
wenzelm@9650
    18
end