src/HOL/Import/HOL/prob_canon.imp
author haftmann
Mon Jan 30 08:20:56 2006 +0100 (2006-01-30)
changeset 18851 9502ce541f01
parent 14516 a183dec876ab
permissions -rw-r--r--
adaptions to codegen_package
skalberg@14516
     1
import
skalberg@14516
     2
skalberg@14516
     3
import_segment "hol4"
skalberg@14516
     4
skalberg@14516
     5
def_maps
skalberg@14516
     6
  "algebra_canon" > "algebra_canon_primdef"
skalberg@14516
     7
  "alg_twinfree" > "alg_twinfree_primdef"
skalberg@14516
     8
  "alg_twin" > "alg_twin_primdef"
skalberg@14516
     9
  "alg_sorted" > "alg_sorted_primdef"
skalberg@14516
    10
  "alg_prefixfree" > "alg_prefixfree_primdef"
skalberg@14516
    11
  "alg_order_tupled" > "alg_order_tupled_def"
skalberg@14516
    12
  "alg_order" > "alg_order_primdef"
skalberg@14516
    13
  "alg_longest" > "alg_longest_primdef"
skalberg@14516
    14
  "alg_canon_prefs" > "alg_canon_prefs_primdef"
skalberg@14516
    15
  "alg_canon_merge" > "alg_canon_merge_primdef"
skalberg@14516
    16
  "alg_canon_find" > "alg_canon_find_primdef"
skalberg@14516
    17
  "alg_canon2" > "alg_canon2_primdef"
skalberg@14516
    18
  "alg_canon1" > "alg_canon1_primdef"
skalberg@14516
    19
  "alg_canon" > "alg_canon_primdef"
skalberg@14516
    20
skalberg@14516
    21
const_maps
skalberg@14516
    22
  "algebra_canon" > "HOL4Prob.prob_canon.algebra_canon"
skalberg@14516
    23
  "alg_twinfree" > "HOL4Prob.prob_canon.alg_twinfree"
skalberg@14516
    24
  "alg_twin" > "HOL4Prob.prob_canon.alg_twin"
skalberg@14516
    25
  "alg_sorted" > "HOL4Prob.prob_canon.alg_sorted"
skalberg@14516
    26
  "alg_prefixfree" > "HOL4Prob.prob_canon.alg_prefixfree"
skalberg@14516
    27
  "alg_order_tupled" > "HOL4Prob.prob_canon.alg_order_tupled"
skalberg@14516
    28
  "alg_order" > "HOL4Prob.prob_canon.alg_order"
skalberg@14516
    29
  "alg_longest" > "HOL4Prob.prob_canon.alg_longest"
skalberg@14516
    30
  "alg_canon2" > "HOL4Prob.prob_canon.alg_canon2"
skalberg@14516
    31
  "alg_canon1" > "HOL4Prob.prob_canon.alg_canon1"
skalberg@14516
    32
  "alg_canon" > "HOL4Prob.prob_canon.alg_canon"
skalberg@14516
    33
skalberg@14516
    34
thm_maps
skalberg@14516
    35
  "algebra_canon_primdef" > "HOL4Prob.prob_canon.algebra_canon_primdef"
skalberg@14516
    36
  "algebra_canon_def" > "HOL4Prob.prob_canon.algebra_canon_def"
skalberg@14516
    37
  "alg_twinfree_primitive_def" > "HOL4Prob.prob_canon.alg_twinfree_primitive_def"
skalberg@14516
    38
  "alg_twinfree_primdef" > "HOL4Prob.prob_canon.alg_twinfree_primdef"
skalberg@14516
    39
  "alg_twinfree_ind" > "HOL4Prob.prob_canon.alg_twinfree_ind"
skalberg@14516
    40
  "alg_twinfree_def" > "HOL4Prob.prob_canon.alg_twinfree_def"
skalberg@14516
    41
  "alg_twin_primdef" > "HOL4Prob.prob_canon.alg_twin_primdef"
skalberg@14516
    42
  "alg_twin_def" > "HOL4Prob.prob_canon.alg_twin_def"
skalberg@14516
    43
  "alg_sorted_primitive_def" > "HOL4Prob.prob_canon.alg_sorted_primitive_def"
skalberg@14516
    44
  "alg_sorted_primdef" > "HOL4Prob.prob_canon.alg_sorted_primdef"
skalberg@14516
    45
  "alg_sorted_ind" > "HOL4Prob.prob_canon.alg_sorted_ind"
skalberg@14516
    46
  "alg_sorted_def" > "HOL4Prob.prob_canon.alg_sorted_def"
skalberg@14516
    47
  "alg_prefixfree_primitive_def" > "HOL4Prob.prob_canon.alg_prefixfree_primitive_def"
skalberg@14516
    48
  "alg_prefixfree_primdef" > "HOL4Prob.prob_canon.alg_prefixfree_primdef"
skalberg@14516
    49
  "alg_prefixfree_ind" > "HOL4Prob.prob_canon.alg_prefixfree_ind"
skalberg@14516
    50
  "alg_prefixfree_def" > "HOL4Prob.prob_canon.alg_prefixfree_def"
skalberg@14516
    51
  "alg_order_tupled_primitive_def" > "HOL4Prob.prob_canon.alg_order_tupled_primitive_def"
skalberg@14516
    52
  "alg_order_tupled_def" > "HOL4Prob.prob_canon.alg_order_tupled_def"
skalberg@14516
    53
  "alg_order_primdef" > "HOL4Prob.prob_canon.alg_order_primdef"
skalberg@14516
    54
  "alg_order_ind" > "HOL4Prob.prob_canon.alg_order_ind"
skalberg@14516
    55
  "alg_order_def" > "HOL4Prob.prob_canon.alg_order_def"
skalberg@14516
    56
  "alg_order_curried_def" > "HOL4Prob.prob_canon.alg_order_curried_def"
skalberg@14516
    57
  "alg_longest_primdef" > "HOL4Prob.prob_canon.alg_longest_primdef"
skalberg@14516
    58
  "alg_longest_def" > "HOL4Prob.prob_canon.alg_longest_def"
skalberg@14516
    59
  "alg_canon_primdef" > "HOL4Prob.prob_canon.alg_canon_primdef"
skalberg@14516
    60
  "alg_canon_prefs_def" > "HOL4Prob.prob_canon.alg_canon_prefs_def"
skalberg@14516
    61
  "alg_canon_merge_def" > "HOL4Prob.prob_canon.alg_canon_merge_def"
skalberg@14516
    62
  "alg_canon_find_def" > "HOL4Prob.prob_canon.alg_canon_find_def"
skalberg@14516
    63
  "alg_canon_def" > "HOL4Prob.prob_canon.alg_canon_def"
skalberg@14516
    64
  "alg_canon2_primdef" > "HOL4Prob.prob_canon.alg_canon2_primdef"
skalberg@14516
    65
  "alg_canon2_def" > "HOL4Prob.prob_canon.alg_canon2_def"
skalberg@14516
    66
  "alg_canon1_primdef" > "HOL4Prob.prob_canon.alg_canon1_primdef"
skalberg@14516
    67
  "alg_canon1_def" > "HOL4Prob.prob_canon.alg_canon1_def"
skalberg@14516
    68
  "MEM_NIL_STEP" > "HOL4Prob.prob_canon.MEM_NIL_STEP"
skalberg@14516
    69
  "ALG_TWIN_SING" > "HOL4Prob.prob_canon.ALG_TWIN_SING"
skalberg@14516
    70
  "ALG_TWIN_REDUCE" > "HOL4Prob.prob_canon.ALG_TWIN_REDUCE"
skalberg@14516
    71
  "ALG_TWIN_NIL" > "HOL4Prob.prob_canon.ALG_TWIN_NIL"
skalberg@14516
    72
  "ALG_TWIN_CONS" > "HOL4Prob.prob_canon.ALG_TWIN_CONS"
skalberg@14516
    73
  "ALG_TWINS_PREFIX" > "HOL4Prob.prob_canon.ALG_TWINS_PREFIX"
skalberg@14516
    74
  "ALG_TWINFREE_TLS" > "HOL4Prob.prob_canon.ALG_TWINFREE_TLS"
skalberg@14516
    75
  "ALG_TWINFREE_TL" > "HOL4Prob.prob_canon.ALG_TWINFREE_TL"
skalberg@14516
    76
  "ALG_TWINFREE_STEP2" > "HOL4Prob.prob_canon.ALG_TWINFREE_STEP2"
skalberg@14516
    77
  "ALG_TWINFREE_STEP1" > "HOL4Prob.prob_canon.ALG_TWINFREE_STEP1"
skalberg@14516
    78
  "ALG_TWINFREE_STEP" > "HOL4Prob.prob_canon.ALG_TWINFREE_STEP"
skalberg@14516
    79
  "ALG_SORTED_TLS" > "HOL4Prob.prob_canon.ALG_SORTED_TLS"
skalberg@14516
    80
  "ALG_SORTED_TL" > "HOL4Prob.prob_canon.ALG_SORTED_TL"
skalberg@14516
    81
  "ALG_SORTED_STEP" > "HOL4Prob.prob_canon.ALG_SORTED_STEP"
skalberg@14516
    82
  "ALG_SORTED_PREFIXFREE_MEM_NIL" > "HOL4Prob.prob_canon.ALG_SORTED_PREFIXFREE_MEM_NIL"
skalberg@14516
    83
  "ALG_SORTED_PREFIXFREE_EQUALITY" > "HOL4Prob.prob_canon.ALG_SORTED_PREFIXFREE_EQUALITY"
skalberg@14516
    84
  "ALG_SORTED_MONO" > "HOL4Prob.prob_canon.ALG_SORTED_MONO"
skalberg@14516
    85
  "ALG_SORTED_MIN" > "HOL4Prob.prob_canon.ALG_SORTED_MIN"
skalberg@14516
    86
  "ALG_SORTED_FILTER" > "HOL4Prob.prob_canon.ALG_SORTED_FILTER"
skalberg@14516
    87
  "ALG_SORTED_DEF_ALT" > "HOL4Prob.prob_canon.ALG_SORTED_DEF_ALT"
skalberg@14516
    88
  "ALG_SORTED_APPEND" > "HOL4Prob.prob_canon.ALG_SORTED_APPEND"
skalberg@14516
    89
  "ALG_PREFIXFREE_TLS" > "HOL4Prob.prob_canon.ALG_PREFIXFREE_TLS"
skalberg@14516
    90
  "ALG_PREFIXFREE_TL" > "HOL4Prob.prob_canon.ALG_PREFIXFREE_TL"
skalberg@14516
    91
  "ALG_PREFIXFREE_STEP" > "HOL4Prob.prob_canon.ALG_PREFIXFREE_STEP"
skalberg@14516
    92
  "ALG_PREFIXFREE_MONO" > "HOL4Prob.prob_canon.ALG_PREFIXFREE_MONO"
skalberg@14516
    93
  "ALG_PREFIXFREE_FILTER" > "HOL4Prob.prob_canon.ALG_PREFIXFREE_FILTER"
skalberg@14516
    94
  "ALG_PREFIXFREE_ELT" > "HOL4Prob.prob_canon.ALG_PREFIXFREE_ELT"
skalberg@14516
    95
  "ALG_PREFIXFREE_APPEND" > "HOL4Prob.prob_canon.ALG_PREFIXFREE_APPEND"
skalberg@14516
    96
  "ALG_ORDER_TRANS" > "HOL4Prob.prob_canon.ALG_ORDER_TRANS"
skalberg@14516
    97
  "ALG_ORDER_TOTAL" > "HOL4Prob.prob_canon.ALG_ORDER_TOTAL"
skalberg@14516
    98
  "ALG_ORDER_SNOC" > "HOL4Prob.prob_canon.ALG_ORDER_SNOC"
skalberg@14516
    99
  "ALG_ORDER_REFL" > "HOL4Prob.prob_canon.ALG_ORDER_REFL"
skalberg@14516
   100
  "ALG_ORDER_PREFIX_TRANS" > "HOL4Prob.prob_canon.ALG_ORDER_PREFIX_TRANS"
skalberg@14516
   101
  "ALG_ORDER_PREFIX_MONO" > "HOL4Prob.prob_canon.ALG_ORDER_PREFIX_MONO"
skalberg@14516
   102
  "ALG_ORDER_PREFIX_ANTI" > "HOL4Prob.prob_canon.ALG_ORDER_PREFIX_ANTI"
skalberg@14516
   103
  "ALG_ORDER_PREFIX" > "HOL4Prob.prob_canon.ALG_ORDER_PREFIX"
skalberg@14516
   104
  "ALG_ORDER_NIL" > "HOL4Prob.prob_canon.ALG_ORDER_NIL"
skalberg@14516
   105
  "ALG_ORDER_ANTISYM" > "HOL4Prob.prob_canon.ALG_ORDER_ANTISYM"
skalberg@14516
   106
  "ALG_LONGEST_TLS" > "HOL4Prob.prob_canon.ALG_LONGEST_TLS"
skalberg@14516
   107
  "ALG_LONGEST_TL" > "HOL4Prob.prob_canon.ALG_LONGEST_TL"
skalberg@14516
   108
  "ALG_LONGEST_HD" > "HOL4Prob.prob_canon.ALG_LONGEST_HD"
skalberg@14516
   109
  "ALG_LONGEST_APPEND" > "HOL4Prob.prob_canon.ALG_LONGEST_APPEND"
skalberg@14516
   110
  "ALG_CANON_SORTED_PREFIXFREE_TWINFREE" > "HOL4Prob.prob_canon.ALG_CANON_SORTED_PREFIXFREE_TWINFREE"
skalberg@14516
   111
  "ALG_CANON_PREFS_SORTED" > "HOL4Prob.prob_canon.ALG_CANON_PREFS_SORTED"
skalberg@14516
   112
  "ALG_CANON_PREFS_PREFIXFREE" > "HOL4Prob.prob_canon.ALG_CANON_PREFS_PREFIXFREE"
skalberg@14516
   113
  "ALG_CANON_PREFS_HD" > "HOL4Prob.prob_canon.ALG_CANON_PREFS_HD"
skalberg@14516
   114
  "ALG_CANON_PREFS_DELETES" > "HOL4Prob.prob_canon.ALG_CANON_PREFS_DELETES"
skalberg@14516
   115
  "ALG_CANON_PREFS_CONSTANT" > "HOL4Prob.prob_canon.ALG_CANON_PREFS_CONSTANT"
skalberg@14516
   116
  "ALG_CANON_MERGE_SORTED_PREFIXFREE_TWINFREE" > "HOL4Prob.prob_canon.ALG_CANON_MERGE_SORTED_PREFIXFREE_TWINFREE"
skalberg@14516
   117
  "ALG_CANON_MERGE_SHORTENS" > "HOL4Prob.prob_canon.ALG_CANON_MERGE_SHORTENS"
skalberg@14516
   118
  "ALG_CANON_MERGE_PREFIXFREE_PRESERVE" > "HOL4Prob.prob_canon.ALG_CANON_MERGE_PREFIXFREE_PRESERVE"
skalberg@14516
   119
  "ALG_CANON_MERGE_CONSTANT" > "HOL4Prob.prob_canon.ALG_CANON_MERGE_CONSTANT"
skalberg@14516
   120
  "ALG_CANON_IDEMPOT" > "HOL4Prob.prob_canon.ALG_CANON_IDEMPOT"
skalberg@14516
   121
  "ALG_CANON_FIND_SORTED" > "HOL4Prob.prob_canon.ALG_CANON_FIND_SORTED"
skalberg@14516
   122
  "ALG_CANON_FIND_PREFIXFREE" > "HOL4Prob.prob_canon.ALG_CANON_FIND_PREFIXFREE"
skalberg@14516
   123
  "ALG_CANON_FIND_HD" > "HOL4Prob.prob_canon.ALG_CANON_FIND_HD"
skalberg@14516
   124
  "ALG_CANON_FIND_DELETES" > "HOL4Prob.prob_canon.ALG_CANON_FIND_DELETES"
skalberg@14516
   125
  "ALG_CANON_FIND_CONSTANT" > "HOL4Prob.prob_canon.ALG_CANON_FIND_CONSTANT"
skalberg@14516
   126
  "ALG_CANON_CONSTANT" > "HOL4Prob.prob_canon.ALG_CANON_CONSTANT"
skalberg@14516
   127
  "ALG_CANON_BASIC" > "HOL4Prob.prob_canon.ALG_CANON_BASIC"
skalberg@14516
   128
  "ALG_CANON2_SORTED_PREFIXFREE_TWINFREE" > "HOL4Prob.prob_canon.ALG_CANON2_SORTED_PREFIXFREE_TWINFREE"
skalberg@14516
   129
  "ALG_CANON2_SHORTENS" > "HOL4Prob.prob_canon.ALG_CANON2_SHORTENS"
skalberg@14516
   130
  "ALG_CANON2_PREFIXFREE_PRESERVE" > "HOL4Prob.prob_canon.ALG_CANON2_PREFIXFREE_PRESERVE"
skalberg@14516
   131
  "ALG_CANON2_CONSTANT" > "HOL4Prob.prob_canon.ALG_CANON2_CONSTANT"
skalberg@14516
   132
  "ALG_CANON1_SORTED" > "HOL4Prob.prob_canon.ALG_CANON1_SORTED"
skalberg@14516
   133
  "ALG_CANON1_PREFIXFREE" > "HOL4Prob.prob_canon.ALG_CANON1_PREFIXFREE"
skalberg@14516
   134
  "ALG_CANON1_CONSTANT" > "HOL4Prob.prob_canon.ALG_CANON1_CONSTANT"
skalberg@14516
   135
  "ALGEBRA_CANON_TLS" > "HOL4Prob.prob_canon.ALGEBRA_CANON_TLS"
skalberg@14516
   136
  "ALGEBRA_CANON_TL" > "HOL4Prob.prob_canon.ALGEBRA_CANON_TL"
skalberg@14516
   137
  "ALGEBRA_CANON_STEP2" > "HOL4Prob.prob_canon.ALGEBRA_CANON_STEP2"
skalberg@14516
   138
  "ALGEBRA_CANON_STEP1" > "HOL4Prob.prob_canon.ALGEBRA_CANON_STEP1"
skalberg@14516
   139
  "ALGEBRA_CANON_STEP" > "HOL4Prob.prob_canon.ALGEBRA_CANON_STEP"
skalberg@14516
   140
  "ALGEBRA_CANON_NIL_MEM" > "HOL4Prob.prob_canon.ALGEBRA_CANON_NIL_MEM"
skalberg@14516
   141
  "ALGEBRA_CANON_INDUCTION" > "HOL4Prob.prob_canon.ALGEBRA_CANON_INDUCTION"
skalberg@14516
   142
  "ALGEBRA_CANON_DEF_ALT" > "HOL4Prob.prob_canon.ALGEBRA_CANON_DEF_ALT"
skalberg@14516
   143
  "ALGEBRA_CANON_CASES_THM" > "HOL4Prob.prob_canon.ALGEBRA_CANON_CASES_THM"
skalberg@14516
   144
  "ALGEBRA_CANON_CASES" > "HOL4Prob.prob_canon.ALGEBRA_CANON_CASES"
skalberg@14516
   145
  "ALGEBRA_CANON_BASIC" > "HOL4Prob.prob_canon.ALGEBRA_CANON_BASIC"
skalberg@14516
   146
skalberg@14516
   147
end