Job 2132

CakeML:73d4774786232785747eb170136ad5ade9ed882c
  Remove trailing whitespace. [May 18 01:34:30]
#954 (pan_parser_funs)
Merging into:5e0612a6f93d34e570019c2a768cbd4736402abe
  Fix for change to finite_mapSyntax in HOL [May 25 02:29:21]
HOL:8a1c5607fb8c5be3be18fbe7a3653c704b0ea4da
  Manual: mention that LaTeX munging handles record types OK [May 23 05:56:07]
Machine:pavlova

May 25 10:27:41 Claimed job