src/HOL/TPTP/mash_eval.ML
changeset 48307 7c78f14d20cf
parent 48303 f1d135d0ea69
child 48311 3c4e10606567
equal deleted inserted replaced
48306:e699f754d9f7 48307:7c78f14d20cf
    15 
    15 
    16 structure MaSh_Eval : MASH_EVAL =
    16 structure MaSh_Eval : MASH_EVAL =
    17 struct
    17 struct
    18 
    18 
    19 open Sledgehammer_Filter_MaSh
    19 open Sledgehammer_Filter_MaSh
    20 
       
    21 val unescape_meta =
       
    22   let
       
    23     fun un accum [] = String.implode (rev accum)
       
    24       | un accum (#"\\" :: d1 :: d2 :: d3 :: cs) =
       
    25         (case Int.fromString (String.implode [d1, d2, d3]) of
       
    26            SOME n => un (Char.chr n :: accum) cs
       
    27          | NONE => "" (* error *))
       
    28       | un _ (#"\\" :: _) = "" (* error *)
       
    29       | un accum (c :: cs) = un (c :: accum) cs
       
    30   in un [] o String.explode end
       
    31 
    20 
    32 val isarN = "Isa"
    21 val isarN = "Isa"
    33 val iterN = "Iter"
    22 val iterN = "Iter"
    34 val mashN = "MaSh"
    23 val mashN = "MaSh"
    35 val meshN = "Mesh"
    24 val meshN = "Mesh"