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