CakeML:fe46ca072678de42c6fdfc32f40eafeb917dab02 Fix proof broken by HOL changes making more rewrites automatic HOL:a6997b93e871c1306b82caf1f7333e32e21c4db0 Reinstate the old xDefine and tDefine functions (at least in bossLib) Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64 Claimed job Reusing HOL