| author | haftmann |
| Thu, 26 Aug 2010 20:51:17 +0200 | |
| changeset 39019 | e46e7a9cb622 |
| parent 37678 | 0040bafffdef |
| child 39028 | 848be46708dc |
| permissions | -rw-r--r-- |
1 (* Title: HOL/Import/Generate-HOLLight/GenHOLLight.thy
2 ID: $Id$
3 Author: Steven Obua (TU Muenchen)
4 *)
6 theory GenHOLLight imports "../HOLLightCompat" "../HOL4Syntax" begin;
8 (*;skip_import_dir "/home/obua/tmp/cache"
10 ;skip_import on*)
12 ;import_segment "hollight";
14 setup_dump "../HOLLight" "HOLLight";
16 append_dump {*theory HOLLight = "../HOLLightCompat" + "../HOL4Syntax":*};
18 ;import_theory hollight;
20 ignore_thms
21 TYDEF_1
22 DEF_one
23 TYDEF_prod
24 TYDEF_num
25 IND_SUC_0_EXISTS
26 DEF__0
27 DEF_SUC
28 DEF_IND_SUC
29 DEF_IND_0
30 DEF_NUM_REP
31 TYDEF_sum
32 DEF_INL
33 DEF_INR
34 (* TYDEF_option*);
36 type_maps
37 ind > Nat.ind
38 bool > bool
39 fun > fun
40 N_1 > Product_Type.unit
41 prod > Product_Type.prod
42 num > Nat.nat
43 sum > Sum_Type.sum
44 (* option > Datatype.option*);
46 const_renames
47 "==" > "eqeq"
48 ".." > "dotdot"
49 "ALL" > ALL_list;
51 const_maps
52 T > True
53 F > False
54 ONE_ONE > HOL4Setup.ONE_ONE
55 ONTO > Fun.surj
56 "=" > "op ="
57 "==>" > HOL.implies
58 "/\\" > "op &"
59 "\\/" > "op |"
60 "!" > All
61 "?" > Ex
62 "?!" > Ex1
63 "~" > Not
64 o > Fun.comp
65 "@" > "Hilbert_Choice.Eps"
66 I > Fun.id
67 one > Product_Type.Unity
68 LET > HOL4Compat.LET
69 mk_pair > Product_Type.Pair_Rep
70 "," > Pair
71 REP_prod > Rep_Prod
72 ABS_prod > Abs_Prod
73 FST > fst
74 SND > snd
75 "_0" > 0 :: nat
76 SUC > Suc
77 PRE > HOLLightCompat.Pred
78 NUMERAL > HOL4Compat.NUMERAL
79 "+" > Groups.plus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
80 "*" > Groups.times :: "nat \<Rightarrow> nat \<Rightarrow> nat"
81 "-" > Groups.minus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
82 BIT0 > HOLLightCompat.NUMERAL_BIT0
83 BIT1 > HOL4Compat.NUMERAL_BIT1
84 INL > Sum_Type.Inl
85 INR > Sum_Type.Inr
86 (* NONE > Datatype.None
87 SOME > Datatype.Some;
88 HAS_SIZE > HOLLightCompat.HAS_SIZE; *)
90 (*import_until "TYDEF_sum"
92 consts
93 print_theorems
95 import_until *)
97 end_import;
99 append_dump "end";
101 flush_dump;
103 import_segment "";
105 end