src/HOL/Tools/ATP/recon_parse.ML
changeset 16840 3d5aad11bc24
parent 16804 3c339e1c069b
child 16953 f025e0dc638b
equal deleted inserted replaced
16839:d7b47195ac7b 16840:3d5aad11bc24
   159 
   159 
   160 
   160 
   161 
   161 
   162 
   162 
   163 fun several p = many (some p)
   163 fun several p = many (some p)
   164       fun collect (h, t) = h ^ (Utils.itlist (fn s1 => fn s2 => s1 ^ s2) t "")
   164       fun collect (h, t) = h ^ (fold_rev (fn s1 => fn s2 => s1 ^ s2) t "")
   165   
   165   
   166       fun lower_letter s = ("a" <= s) andalso (s <= "z")
   166       fun lower_letter s = ("a" <= s) andalso (s <= "z")
   167       fun upper_letter s = ("A" <= s) andalso (s <= "Z")
   167       fun upper_letter s = ("A" <= s) andalso (s <= "Z")
   168       fun digit s = ("0" <= s) andalso (s <= "9")
   168       fun digit s = ("0" <= s) andalso (s <= "9")
   169       fun letter s = lower_letter s orelse upper_letter s
   169       fun letter s = lower_letter s orelse upper_letter s