src/HOL/Main.thy
author berghofe
Mon Dec 16 13:43:11 2002 +0100 (2002-12-16)
changeset 13755 a9bb54a3cfb7
parent 13403 bc2b32ee62fd
child 14049 ef1da11a64b9
permissions -rw-r--r--
Added mk_int and mk_list.
nipkow@10519
     1
(*  Title:      HOL/Main.thy
nipkow@10519
     2
    ID:         $Id$
wenzelm@12024
     3
    Author:     Stefan Berghofer, Tobias Nipkow and Markus Wenzel, TU Muenchen
wenzelm@12024
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
nipkow@10519
     5
*)
wenzelm@9619
     6
wenzelm@12024
     7
header {* Main HOL *}
wenzelm@12024
     8
berghofe@13403
     9
theory Main = Map + Hilbert_Choice + Extraction:
wenzelm@9650
    10
wenzelm@12024
    11
text {*
wenzelm@12024
    12
  Theory @{text Main} includes everything.  Note that theory @{text
wenzelm@12024
    13
  PreList} already includes most HOL theories.
wenzelm@12024
    14
*}
wenzelm@12024
    15
wenzelm@12024
    16
subsection {* Configuration of the code generator *}
berghofe@11533
    17
berghofe@11533
    18
types_code
berghofe@11533
    19
  "bool"  ("bool")
berghofe@12439
    20
  "*"     ("(_ */ _)")
berghofe@12439
    21
  "list"  ("_ list")
berghofe@11533
    22
berghofe@11533
    23
consts_code
berghofe@11533
    24
  "op ="    ("(_ =/ _)")
berghofe@11533
    25
berghofe@11533
    26
  "True"    ("true")
berghofe@11533
    27
  "False"   ("false")
berghofe@11533
    28
  "Not"     ("not")
berghofe@11533
    29
  "op |"    ("(_ orelse/ _)")
berghofe@11533
    30
  "op &"    ("(_ andalso/ _)")
berghofe@11533
    31
  "If"      ("(if _/ then _/ else _)")
berghofe@11533
    32
berghofe@11533
    33
  "Pair"    ("(_,/ _)")
berghofe@11533
    34
  "fst"     ("fst")
berghofe@11533
    35
  "snd"     ("snd")
berghofe@11533
    36
berghofe@11533
    37
  "Nil"     ("[]")
berghofe@11533
    38
  "Cons"    ("(_ ::/ _)")
berghofe@12439
    39
berghofe@13093
    40
  "wfrec"   ("wf'_rec?")
berghofe@13093
    41
berghofe@13755
    42
ML {*
berghofe@13755
    43
fun wf_rec f x = f (wf_rec f) x;
berghofe@13755
    44
berghofe@13755
    45
val term_of_list = HOLogic.mk_list;
berghofe@13755
    46
val term_of_int = HOLogic.mk_int;
berghofe@13755
    47
*}
berghofe@13093
    48
berghofe@12554
    49
lemma [code]: "((n::nat) < 0) = False" by simp
berghofe@12554
    50
declare less_Suc_eq [code]
berghofe@12554
    51
wenzelm@9650
    52
end