| author | wenzelm |
| Sat, 03 Mar 2012 22:53:24 +0100 | |
| changeset 46793 | 3bbc156823dd |
| parent 46787 | 3d3d8f8929a7 |
| permissions | -rw-r--r-- |
| 14516 | 1 |
import |
2 |
||
3 |
import_segment "hol4" |
|
4 |
||
5 |
def_maps |
|
6 |
"RPROD" > "RPROD_def" |
|
7 |
"LEX" > "LEX_def" |
|
8 |
||
9 |
type_maps |
|
|
37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37591
diff
changeset
|
10 |
"prod" > "Product_Type.prod" |
| 14516 | 11 |
|
12 |
const_maps |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
40607
diff
changeset
|
13 |
"pair_case" > "Product_Type.prod.prod_case" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
40607
diff
changeset
|
14 |
"UNCURRY" > "Product_Type.prod.prod_case" |
| 37391 | 15 |
"SND" > "Product_Type.snd" |
| 14516 | 16 |
"RPROD" > "HOL4Base.pair.RPROD" |
17 |
"LEX" > "HOL4Base.pair.LEX" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
40607
diff
changeset
|
18 |
"FST" > "Product_Type.fst" |
|
37387
3581483cca6c
qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
haftmann
parents:
17916
diff
changeset
|
19 |
"CURRY" > "Product_Type.curry" |
| 37391 | 20 |
"," > "Product_Type.Pair" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
40607
diff
changeset
|
21 |
"##" > "Product_Type.map_pair" |
| 14516 | 22 |
|
23 |
thm_maps |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
40607
diff
changeset
|
24 |
"pair_induction" > "Product_Type.prod.induct" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
40607
diff
changeset
|
25 |
"pair_case_thm" > "Product_Type.prod.cases" |
|
46787
3d3d8f8929a7
file system structure separating HOL4 and HOL Light concerns
haftmann
parents:
44763
diff
changeset
|
26 |
"pair_case_def" > "Compatibility.pair_case_def" |
| 14516 | 27 |
"pair_case_cong" > "HOL4Base.pair.pair_case_cong" |
28 |
"pair_Axiom" > "HOL4Base.pair.pair_Axiom" |
|
29 |
"WF_RPROD" > "HOL4Base.pair.WF_RPROD" |
|
30 |
"WF_LEX" > "HOL4Base.pair.WF_LEX" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
40607
diff
changeset
|
31 |
"UNCURRY_VAR" > "Product_Type.prod_case_beta" |
| 14516 | 32 |
"UNCURRY_ONE_ONE_THM" > "HOL4Base.pair.UNCURRY_ONE_ONE_THM" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
40607
diff
changeset
|
33 |
"UNCURRY_DEF" > "Product_Type.prod.cases" |
| 14516 | 34 |
"UNCURRY_CURRY_THM" > "Product_Type.split_curry" |
35 |
"UNCURRY_CONG" > "HOL4Base.pair.UNCURRY_CONG" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
40607
diff
changeset
|
36 |
"UNCURRY" > "Product_Type.prod_case_beta" |
| 14516 | 37 |
"SND" > "Product_Type.snd_conv" |
38 |
"RPROD_def" > "HOL4Base.pair.RPROD_def" |
|
39 |
"RPROD_DEF" > "HOL4Base.pair.RPROD_DEF" |
|
40 |
"PFORALL_THM" > "HOL4Base.pair.PFORALL_THM" |
|
41 |
"PEXISTS_THM" > "HOL4Base.pair.PEXISTS_THM" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
40607
diff
changeset
|
42 |
"PAIR_MAP_THM" > "Product_Type.map_pair_simp" |
|
46787
3d3d8f8929a7
file system structure separating HOL4 and HOL Light concerns
haftmann
parents:
44763
diff
changeset
|
43 |
"PAIR_MAP" > "Compatibility.PAIR_MAP" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
40607
diff
changeset
|
44 |
"PAIR_EQ" > "Product_Type.Pair_eq" |
|
46787
3d3d8f8929a7
file system structure separating HOL4 and HOL Light concerns
haftmann
parents:
44763
diff
changeset
|
45 |
"PAIR" > "Compatibility.PAIR" |
| 14516 | 46 |
"LEX_def" > "HOL4Base.pair.LEX_def" |
47 |
"LEX_DEF" > "HOL4Base.pair.LEX_DEF" |
|
48 |
"LET2_RATOR" > "HOL4Base.pair.LET2_RATOR" |
|
49 |
"LET2_RAND" > "HOL4Base.pair.LET2_RAND" |
|
50 |
"LAMBDA_PROD" > "Product_Type.split_eta" |
|
51 |
"FST" > "Product_Type.fst_conv" |
|
52 |
"FORALL_PROD" > "Product_Type.split_paired_All" |
|
53 |
"EXISTS_PROD" > "Product_Type.split_paired_Ex" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
40607
diff
changeset
|
54 |
"ELIM_UNCURRY" > "Product_Type.prod_case_beta" |
| 14516 | 55 |
"ELIM_PFORALL" > "HOL4Base.pair.ELIM_PFORALL" |
56 |
"ELIM_PEXISTS" > "HOL4Base.pair.ELIM_PEXISTS" |
|
57 |
"CURRY_UNCURRY_THM" > "Product_Type.curry_split" |
|
58 |
"CURRY_ONE_ONE_THM" > "HOL4Base.pair.CURRY_ONE_ONE_THM" |
|
59 |
"CURRY_DEF" > "Product_Type.curry_conv" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
40607
diff
changeset
|
60 |
"CLOSED_PAIR_EQ" > "Product_Type.Pair_eq" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
40607
diff
changeset
|
61 |
"ABS_PAIR_THM" > "Product_Type.prod.nchotomy" |
| 14516 | 62 |
|
63 |
ignore_thms |
|
64 |
"prod_TY_DEF" |
|
65 |
"MK_PAIR_DEF" |
|
66 |
"IS_PAIR_DEF" |
|
67 |
"COMMA_DEF" |
|
68 |
"ABS_REP_prod" |
|
69 |
||
70 |
end |