1structure Symbolic :> Symbolic = 2struct 3 4val symb_map = [("Type", "-->", "arrow"), 5 ("Lib", "|->", "maplet"), 6 ("Lib", "##", "hash2"), 7 ("bossLib", "&&", "amper2"), 8 ("BasicProvers", "&&", "amper2"), 9 ("simpLib", "++", "plus2"), 10 ("Parse", "--", "minus2"), 11 ("Parse", "==", "equal2")]; 12 13fun unsymb "Type.-->" = "Type.arrow" 14 | unsymb "Lib.|->" = "Lib.maplet" 15 | unsymb "Lib.\\#\\#" = "Lib.hash2" 16 | unsymb "Lib.|>" = "Lib.pipegt" 17 | unsymb "Lib.##" = "Lib.hash2" 18 | unsymb "bossLib.&&" = "bossLib.amper2" 19 | unsymb "BasicProvers.&&" = "BasicProvers.amper2" 20 | unsymb "simpLib.++" = "simpLib.plus2" 21 | unsymb "bossLib.++" = "bossLib.plus2" 22 | unsymb "Parse.--" = "Parse.minus2" 23 | unsymb "Parse.==" = "Parse.equal2" 24 | unsymb other = other; 25 26fun tosymb "Type.arrow" = "Type.-->" 27 | tosymb "Lib.maplet" = "Lib.|->" 28 | tosymb "Lib.pipegt" = "Lib.|>" 29 | tosymb "Lib.hash2" = "Lib.##" 30 | tosymb "bossLib.amper2" = "bossLib.&&" 31 | tosymb "BasicProvers.amper2" = "BasicProvers.&&" 32 | tosymb "simpLib.plus2" = "simpLib.++" 33 | tosymb "Parse.minus2" = "Parse.--" 34 | tosymb "Parse.equal2" = "Parse.==" 35 | tosymb other = other; 36 37end 38