--- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Fri Sep 16 20:30:44 2005 +0200
+++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Fri Sep 16 21:02:15 2005 +0200
@@ -28,9 +28,9 @@
DEF_IND_SUC
DEF_IND_0
DEF_NUM_REP
- TYDEF_sum
+ (* TYDEF_sum
DEF_INL
- DEF_INR;
+ DEF_INR*);
type_maps
ind > Nat.ind
@@ -38,8 +38,8 @@
fun > fun
N_1 > Product_Type.unit
prod > "*"
- num > nat
- sum > "+";
+ num > nat;
+ (* sum > "+";*)
const_maps
T > True
@@ -73,9 +73,17 @@
"*" > "op *" :: "nat \<Rightarrow> nat \<Rightarrow> nat"
"-" > "op -" :: "nat \<Rightarrow> nat \<Rightarrow> nat"
BIT0 > HOLLightCompat.NUMERAL_BIT0
- BIT1 > HOL4Compat.NUMERAL_BIT1
- INL > Sum_Type.Inl
- INR > Sum_Type.Inr;
+ BIT1 > HOL4Compat.NUMERAL_BIT1;
+ (* INL > Sum_Type.Inl
+ INR > Sum_Type.Inr
+ HAS_SIZE > HOLLightCompat.HAS_SIZE*)
+
+(*import_until "TYDEF_sum"
+
+consts
+print_theorems
+
+import_until *)
end_import;