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