src/HOL/Import/Generate-HOLLight/GenHOLLight.thy
author wenzelm
Thu May 27 18:10:37 2010 +0200 (2010-05-27)
changeset 37146 f652333bbf8e
parent 35267 8dfd816713c6
child 37391 476270a6c2dc
permissions -rw-r--r--
renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
     1 (*  Title:      HOL/Import/Generate-HOLLight/GenHOLLight.thy
     2     ID:         $Id$
     3     Author:     Steven Obua (TU Muenchen)
     4 *)
     5 
     6 theory GenHOLLight imports "../HOLLightCompat" "../HOL4Syntax" begin;
     7 
     8 (*;skip_import_dir "/home/obua/tmp/cache"
     9 
    10 ;skip_import on*)
    11 
    12 ;import_segment "hollight";
    13 
    14 setup_dump "../HOLLight" "HOLLight";
    15 
    16 append_dump {*theory HOLLight = "../HOLLightCompat" + "../HOL4Syntax":*};
    17 
    18 ;import_theory hollight;
    19 
    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*);
    35 
    36 type_maps
    37   ind > Nat.ind
    38   bool > bool
    39   fun > fun
    40   N_1 >  Product_Type.unit
    41   prod > "*"
    42   num > nat
    43   sum > "+"
    44 (*  option > Datatype.option*);
    45 
    46 const_renames
    47   "==" > "eqeq"
    48   ".." > "dotdot"
    49   "ALL" > ALL_list;
    50 
    51 const_maps
    52   T > True
    53   F > False
    54   ONE_ONE > HOL4Setup.ONE_ONE
    55   ONTO    > Fun.surj
    56   "=" > "op ="
    57   "==>" > "op -->"
    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; *)
    89 
    90 (*import_until "TYDEF_sum"
    91 
    92 consts
    93 print_theorems
    94 
    95 import_until *)
    96 
    97 end_import;
    98 
    99 append_dump "end";
   100 
   101 flush_dump;
   102 
   103 import_segment "";
   104 
   105 end