author | haftmann |
Thu, 28 Jan 2010 11:48:49 +0100 | |
changeset 34974 | 18b41bba42b5 |
parent 23881 | 851c74f1bb69 |
child 35092 | cfe605c54e50 |
permissions | -rw-r--r-- |
14516 | 1 |
import |
2 |
||
3 |
import_segment "hol4" |
|
4 |
||
5 |
def_maps |
|
6 |
"wellfounded" > "wellfounded_primdef" |
|
7 |
"measure" > "measure_primdef" |
|
8 |
"SIMP_REC_REL" > "SIMP_REC_REL_def" |
|
9 |
"SIMP_REC" > "SIMP_REC_def" |
|
10 |
"PRIM_REC_FUN" > "PRIM_REC_FUN_def" |
|
11 |
"PRIM_REC" > "PRIM_REC_def" |
|
12 |
"PRE" > "PRE_def" |
|
13 |
||
14 |
const_maps |
|
15 |
"wellfounded" > "HOL4Base.prim_rec.wellfounded" |
|
16 |
"measure" > "HOL4Base.prim_rec.measure" |
|
17 |
"SIMP_REC_REL" > "HOL4Base.prim_rec.SIMP_REC_REL" |
|
18 |
"PRIM_REC_FUN" > "HOL4Base.prim_rec.PRIM_REC_FUN" |
|
19 |
"PRIM_REC" > "HOL4Base.prim_rec.PRIM_REC" |
|
20 |
"PRE" > "HOL4Base.prim_rec.PRE" |
|
34974
18b41bba42b5
new theory Algebras.thy for generic algebraic structures
haftmann
parents:
23881
diff
changeset
|
21 |
"<" > "Algebras.less" :: "nat => nat => bool" |
14516 | 22 |
|
23 |
thm_maps |
|
24 |
"wellfounded_primdef" > "HOL4Base.prim_rec.wellfounded_primdef" |
|
25 |
"wellfounded_def" > "HOL4Base.prim_rec.wellfounded_def" |
|
26 |
"num_Axiom_old" > "HOL4Base.prim_rec.num_Axiom_old" |
|
27 |
"num_Axiom" > "HOL4Base.prim_rec.num_Axiom" |
|
28 |
"measure_thm" > "HOL4Base.prim_rec.measure_thm" |
|
29 |
"measure_primdef" > "HOL4Base.prim_rec.measure_primdef" |
|
30 |
"measure_def" > "HOL4Base.prim_rec.measure_def" |
|
31 |
"WF_measure" > "HOL4Base.prim_rec.WF_measure" |
|
32 |
"WF_PRED" > "HOL4Base.prim_rec.WF_PRED" |
|
33 |
"WF_LESS" > "HOL4Base.prim_rec.WF_LESS" |
|
34 |
"WF_IFF_WELLFOUNDED" > "HOL4Base.prim_rec.WF_IFF_WELLFOUNDED" |
|
35 |
"SUC_LESS" > "Nat.Suc_lessD" |
|
36 |
"SUC_ID" > "Nat.Suc_n_not_n" |
|
37 |
"SIMP_REC_THM" > "HOL4Base.prim_rec.SIMP_REC_THM" |
|
38 |
"SIMP_REC_REL_def" > "HOL4Base.prim_rec.SIMP_REC_REL_def" |
|
39 |
"SIMP_REC_REL_UNIQUE_RESULT" > "HOL4Base.prim_rec.SIMP_REC_REL_UNIQUE_RESULT" |
|
40 |
"SIMP_REC_REL_UNIQUE" > "HOL4Base.prim_rec.SIMP_REC_REL_UNIQUE" |
|
41 |
"SIMP_REC_REL" > "HOL4Base.prim_rec.SIMP_REC_REL" |
|
42 |
"SIMP_REC_EXISTS" > "HOL4Base.prim_rec.SIMP_REC_EXISTS" |
|
43 |
"SIMP_REC" > "HOL4Base.prim_rec.SIMP_REC" |
|
44 |
"PRIM_REC_def" > "HOL4Base.prim_rec.PRIM_REC_def" |
|
45 |
"PRIM_REC_THM" > "HOL4Base.prim_rec.PRIM_REC_THM" |
|
46 |
"PRIM_REC_FUN_def" > "HOL4Base.prim_rec.PRIM_REC_FUN_def" |
|
47 |
"PRIM_REC_FUN" > "HOL4Base.prim_rec.PRIM_REC_FUN" |
|
48 |
"PRIM_REC_EQN" > "HOL4Base.prim_rec.PRIM_REC_EQN" |
|
49 |
"PRIM_REC" > "HOL4Base.prim_rec.PRIM_REC" |
|
50 |
"PRE_def" > "HOL4Base.prim_rec.PRE_def" |
|
51 |
"PRE_DEF" > "HOL4Base.prim_rec.PRE_DEF" |
|
52 |
"PRE" > "HOL4Base.prim_rec.PRE" |
|
53 |
"NOT_LESS_EQ" > "HOL4Base.prim_rec.NOT_LESS_EQ" |
|
54 |
"NOT_LESS_0" > "Nat.not_less0" |
|
55 |
"LESS_THM" > "HOL4Base.prim_rec.LESS_THM" |
|
56 |
"LESS_SUC_SUC" > "HOL4Base.prim_rec.LESS_SUC_SUC" |
|
57 |
"LESS_SUC_REFL" > "Nat.lessI" |
|
58 |
"LESS_SUC_IMP" > "HOL4Base.prim_rec.LESS_SUC_IMP" |
|
59 |
"LESS_SUC" > "Nat.less_SucI" |
|
60 |
"LESS_REFL" > "Nat.less_not_refl" |
|
61 |
"LESS_NOT_EQ" > "Nat.less_not_refl3" |
|
62 |
"LESS_MONO" > "Nat.Suc_mono" |
|
63 |
"LESS_LEMMA2" > "HOL4Base.prim_rec.LESS_LEMMA2" |
|
64 |
"LESS_LEMMA1" > "HOL4Base.prim_rec.LESS_LEMMA1" |
|
65 |
"LESS_DEF" > "HOL4Compat.LESS_DEF" |
|
66 |
"LESS_0_0" > "HOL4Base.prim_rec.LESS_0_0" |
|
67 |
"LESS_0" > "Nat.zero_less_Suc" |
|
68 |
"INV_SUC_EQ" > "Nat.nat.simps_3" |
|
69 |
"EQ_LESS" > "HOL4Base.prim_rec.EQ_LESS" |
|
70 |
"DC" > "HOL4Base.prim_rec.DC" |
|
71 |
||
72 |
end |