--- a/src/HOL/Import/HOL4/Generated/num.imp Sun Apr 01 14:50:47 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-import
-
-import_segment "hol4"
-
-type_maps
- "num" > "Nat.nat"
-
-const_maps
- "SUC" > "Nat.Suc"
- "0" > "Groups.zero_class.zero" :: "nat"
-
-thm_maps
- "NOT_SUC" > "Nat.Suc_not_Zero"
- "INV_SUC" > "Nat.Suc_inject"
- "INDUCTION" > "Fact.fact_nat.induct"
-
-ignore_thms
- "num_TY_DEF"
- "num_ISO_DEF"
- "ZERO_REP_DEF"
- "ZERO_DEF"
- "SUC_REP_DEF"
- "SUC_DEF"
- "IS_NUM_REP"
-
-end