| author | wenzelm |
| Tue, 06 Aug 2002 11:22:05 +0200 | |
| changeset 13462 | 56610e2ba220 |
| parent 13403 | bc2b32ee62fd |
| child 13755 | a9bb54a3cfb7 |
| permissions | -rw-r--r-- |
| 10519 | 1 |
(* Title: HOL/Main.thy |
2 |
ID: $Id$ |
|
| 12024 | 3 |
Author: Stefan Berghofer, Tobias Nipkow and Markus Wenzel, TU Muenchen |
4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
| 10519 | 5 |
*) |
| 9619 | 6 |
|
| 12024 | 7 |
header {* Main HOL *}
|
8 |
||
| 13403 | 9 |
theory Main = Map + Hilbert_Choice + Extraction: |
|
9650
6f0b89f2a1f9
Main now new-style theory; added Main.ML for compatibility;
wenzelm
parents:
9619
diff
changeset
|
10 |
|
| 12024 | 11 |
text {*
|
12 |
Theory @{text Main} includes everything. Note that theory @{text
|
|
13 |
PreList} already includes most HOL theories. |
|
14 |
*} |
|
15 |
||
16 |
subsection {* Configuration of the code generator *}
|
|
| 11533 | 17 |
|
18 |
types_code |
|
19 |
"bool" ("bool")
|
|
| 12439 | 20 |
"*" ("(_ */ _)")
|
21 |
"list" ("_ list")
|
|
| 11533 | 22 |
|
23 |
consts_code |
|
24 |
"op =" ("(_ =/ _)")
|
|
25 |
||
26 |
"True" ("true")
|
|
27 |
"False" ("false")
|
|
28 |
"Not" ("not")
|
|
29 |
"op |" ("(_ orelse/ _)")
|
|
30 |
"op &" ("(_ andalso/ _)")
|
|
31 |
"If" ("(if _/ then _/ else _)")
|
|
32 |
||
33 |
"Pair" ("(_,/ _)")
|
|
34 |
"fst" ("fst")
|
|
35 |
"snd" ("snd")
|
|
36 |
||
37 |
"Nil" ("[]")
|
|
38 |
"Cons" ("(_ ::/ _)")
|
|
| 12439 | 39 |
|
|
13093
ab0335307905
code generator: wfrec combinator is now implemented by ML function wf_rec.
berghofe
parents:
12554
diff
changeset
|
40 |
"wfrec" ("wf'_rec?")
|
|
ab0335307905
code generator: wfrec combinator is now implemented by ML function wf_rec.
berghofe
parents:
12554
diff
changeset
|
41 |
|
|
ab0335307905
code generator: wfrec combinator is now implemented by ML function wf_rec.
berghofe
parents:
12554
diff
changeset
|
42 |
ML {* fun wf_rec f x = f (wf_rec f) x; *}
|
|
ab0335307905
code generator: wfrec combinator is now implemented by ML function wf_rec.
berghofe
parents:
12554
diff
changeset
|
43 |
|
|
12554
671b4d632c34
Declared characteristic equations for < on nat for code generation.
berghofe
parents:
12439
diff
changeset
|
44 |
lemma [code]: "((n::nat) < 0) = False" by simp |
|
671b4d632c34
Declared characteristic equations for < on nat for code generation.
berghofe
parents:
12439
diff
changeset
|
45 |
declare less_Suc_eq [code] |
|
671b4d632c34
Declared characteristic equations for < on nat for code generation.
berghofe
parents:
12439
diff
changeset
|
46 |
|
|
9650
6f0b89f2a1f9
Main now new-style theory; added Main.ML for compatibility;
wenzelm
parents:
9619
diff
changeset
|
47 |
end |