src/HOL/Main.thy
author paulson
Wed Aug 08 14:52:10 2001 +0200 (2001-08-08)
changeset 11483 f4d10044a2cd
parent 10519 ade64af4c57c
child 11533 0c0d2332e8f0
permissions -rw-r--r--
Hilbert_Choice is needed only in Main itself
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
paulson@11483
    10
theory Main = Map + String + Hilbert_Choice:
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