nipkow@10519: (*  Title:      HOL/Main.thy
nipkow@10519:     ID:         $Id$
wenzelm@12024:     Author:     Stefan Berghofer, Tobias Nipkow and Markus Wenzel, TU Muenchen
wenzelm@12024:     License:    GPL (GNU GENERAL PUBLIC LICENSE)
nipkow@10519: *)
wenzelm@9619: 
wenzelm@12024: header {* Main HOL *}
wenzelm@12024: 
berghofe@13403: theory Main = Map + Hilbert_Choice + Extraction:
wenzelm@9650: 
wenzelm@12024: text {*
wenzelm@12024:   Theory @{text Main} includes everything.  Note that theory @{text
wenzelm@12024:   PreList} already includes most HOL theories.
wenzelm@12024: *}
wenzelm@12024: 
wenzelm@12024: subsection {* Configuration of the code generator *}
berghofe@11533: 
berghofe@11533: types_code
berghofe@11533:   "bool"  ("bool")
berghofe@12439:   "*"     ("(_ */ _)")
berghofe@12439:   "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@12439: 
berghofe@13093:   "wfrec"   ("wf'_rec?")
berghofe@13093: 
berghofe@13755: ML {*
berghofe@13755: fun wf_rec f x = f (wf_rec f) x;
berghofe@13755: 
berghofe@13755: val term_of_list = HOLogic.mk_list;
berghofe@13755: val term_of_int = HOLogic.mk_int;
berghofe@13755: *}
berghofe@13093: 
berghofe@12554: lemma [code]: "((n::nat) < 0) = False" by simp
berghofe@12554: declare less_Suc_eq [code]
berghofe@12554: 
wenzelm@9650: end