1 2open HolKernel Parse DB testutils 3 4val _ = set_trace "Unicode" 0 5 6val _ = tprint "test of apropos_in, find_in" 7 8val _ = let 9 val str = "THM" ; 10 val tm = ``$/\`` ; 11 val find1 = find str ; 12 val list1 = apropos_in tm find1 ; 13 val apropos2 = apropos tm ; 14 val list2 = find_in str apropos2 ; 15 val true = length list1 = length list2 ; 16 (* next test may be implementation dependent *) 17 val true = map #1 list1 = map #1 list2 ; 18in OK() end handle _ => die "FAILED" ; 19