author | berghofe |
Fri, 31 Aug 2001 16:28:26 +0200 | |
changeset 11533 | 0c0d2332e8f0 |
parent 11483 | f4d10044a2cd |
child 12024 | b3661262541e |
permissions | -rw-r--r-- |
10519 | 1 |
(* Title: HOL/Main.thy |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow |
|
4 |
Copyright 2000 TU Muenchen |
|
9619 | 5 |
|
10519 | 6 |
Theory Main includes everything. |
7 |
Note that theory PreList already includes most HOL theories. |
|
8 |
*) |
|
9619 | 9 |
|
11483 | 10 |
theory Main = Map + String + Hilbert_Choice: |
9650
6f0b89f2a1f9
Main now new-style theory; added Main.ML for compatibility;
wenzelm
parents:
9619
diff
changeset
|
11 |
|
10261 | 12 |
(*belongs to theory List*) |
13 |
declare lists_mono [mono] |
|
14 |
declare map_cong [recdef_cong] |
|
10386 | 15 |
lemmas rev_induct [case_names Nil snoc] = rev_induct |
16 |
and rev_cases [case_names Nil snoc] = rev_exhaust |
|
9768 | 17 |
|
11533 | 18 |
(** configuration of code generator **) |
19 |
||
20 |
types_code |
|
21 |
"bool" ("bool") |
|
22 |
"*" ("prod") |
|
23 |
"list" ("list") |
|
24 |
||
25 |
consts_code |
|
26 |
"op =" ("(_ =/ _)") |
|
27 |
||
28 |
"True" ("true") |
|
29 |
"False" ("false") |
|
30 |
"Not" ("not") |
|
31 |
"op |" ("(_ orelse/ _)") |
|
32 |
"op &" ("(_ andalso/ _)") |
|
33 |
"If" ("(if _/ then _/ else _)") |
|
34 |
||
35 |
"Pair" ("(_,/ _)") |
|
36 |
"fst" ("fst") |
|
37 |
"snd" ("snd") |
|
38 |
||
39 |
"Nil" ("[]") |
|
40 |
"Cons" ("(_ ::/ _)") |
|
41 |
||
9650
6f0b89f2a1f9
Main now new-style theory; added Main.ML for compatibility;
wenzelm
parents:
9619
diff
changeset
|
42 |
end |