
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: 
paulson@11483: theory Main = Map + String + Hilbert_Choice:
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: 
berghofe@11533: (** configuration of code generator **)
berghofe@11533: 
berghofe@11533: types_code
berghofe@11533:   "bool"  ("bool")
berghofe@11533:   "*"     ("prod")
berghofe@11533:   "list"  ("list")
berghofe@11533: 
berghofe@11533: consts_code
berghofe@11533:   "op ="    ("(_ =/ _)")
berghofe@11533: 
berghofe@11533:   "True"    ("true")
berghofe@11533:   "False"   ("false")
berghofe@11533:   "Not"     ("not")
berghofe@11533:   "op |"    ("(_ orelse/ _)")
berghofe@11533:   "op &"    ("(_ andalso/ _)")
berghofe@11533:   "If"      ("(if _/ then _/ else _)")
berghofe@11533: 
berghofe@11533:   "Pair"    ("(_,/ _)")
berghofe@11533:   "fst"     ("fst")
berghofe@11533:   "snd"     ("snd")
berghofe@11533: 
berghofe@11533:   "Nil"     ("[]")
berghofe@11533:   "Cons"    ("(_ ::/ _)")
berghofe@11533:   
wenzelm@9650: end




