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