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