Job 621

  Merge branch 'origin/master' into local
#577 (local)
Merging into:fc7210e6e390f10177982607373a07ef1e4b5808
  Update for new s-expression syntax (using 
  Slightly extend documentation of fn-update syntax with more example
Machine:oven1 4.15.9-300.fc27.x86_64 x86_64 GNU/Linux

 Claimed job
 Building HOL
 Starting developers
 Finished developers                                               2s  21MB
 Starting developers/bin
 Finished developers/bin                                        1m06s 916MB
 Starting semantics/ffi
 Finished semantics/ffi                                           38s 493MB
 Starting semantics
 Finished semantics                                             1m35s   1GB
 Starting semantics/proofs
 Finished semantics/proofs                                      3m02s   1GB
 Starting basis/pure
 Finished basis/pure                                            3m38s 694MB
 Starting translator
 Finished translator                                            1m17s 879MB
 Starting compiler/parsing
 Finished compiler/parsing                                      1m15s   1GB
 Starting characteristic
 Finished characteristic                                        2m37s   1GB
 Starting translator/monadic
 Finished translator/monadic                                    1m30s   1GB
 Starting basis
 Finished basis                                                16m25s   3GB
 Starting compiler/inference
 Finished compiler/inference                                    1m59s   1GB
 Starting compiler/backend/reg_alloc
 Finished compiler/backend/reg_alloc                              49s   1GB
 Starting compiler/backend/gc