src/HOL/Main.thy
author berghofe
Sun Jul 21 15:42:30 2002 +0200 (2002-07-21)
changeset 13403 bc2b32ee62fd
parent 13367 ad307f0d80db
child 13755 a9bb54a3cfb7
permissions -rw-r--r--
Added theory for setting up program extraction.
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@13093
    42
ML {* fun wf_rec f x = f (wf_rec f) x; *}
berghofe@13093
    43
berghofe@12554
    44
lemma [code]: "((n::nat) < 0) = False" by simp
berghofe@12554
    45
declare less_Suc_eq [code]
berghofe@12554
    46
wenzelm@9650
    47
end