src/HOL/Tools/function_package/lexicographic_order.ML
changeset 21510 7e72185e4b24
parent 21319 cf814e36f788
child 21590 ef7278f553eb
equal deleted inserted replaced
21509:6c5755ad9cae 21510:7e72185e4b24
     6 *)
     6 *)
     7 
     7 
     8 signature LEXICOGRAPHIC_ORDER =
     8 signature LEXICOGRAPHIC_ORDER =
     9 sig
     9 sig
    10   val lexicographic_order : Proof.context -> Method.method
    10   val lexicographic_order : Proof.context -> Method.method
       
    11 
       
    12   (* exported for use by size-change termination prototype.
       
    13      FIXME: provide a common interface later *)
       
    14   val mk_base_funs : typ -> term list
       
    15 
    11   val setup: theory -> theory
    16   val setup: theory -> theory
    12 end
    17 end
    13 
    18 
    14 structure LexicographicOrder : LEXICOGRAPHIC_ORDER =
    19 structure LexicographicOrder : LEXICOGRAPHIC_ORDER =
    15 struct
    20 struct