removed some cheats, tagged a few others as easy
progress on x64CorrectScript.sml
more progress on x64CorrectScript.sml
delete a stray '<' in x64_heapScript.sml
prove env_rs_repl_decs_inp_out
progress on x64Correct
add more things to x86-64's heap

pre-load the big theories.
haven't tested whether this breaks anything - about to.
fix proof in ml_heapScript.sml

probably broken by something in the change to the HOLHEAP
fix proofs in x64_heapScript.sml

probably broken by something in the change to the HOLHEAP
work on x64CorrectScript.sml - essentially finished now

there are some cheats left in it, which are things that should have been
proved elsewhere but weren't.
made code_install less partial
prove a cheat in x64_heapScript.sml
prove a cheat in x64_heapScript.sml
prove another cheat in x64_heapScript.sml
prove another cheat in x64_heapScript.sml
prove another x64_heapScript.sml cheat

that's the last one labelled as locally provable
comment out a cheat in x64CorrectScript.sml

it is not necessary for the exported theorems
progress on x64Correct
a bit more progress on x64Correct
yet more progess on x64Correct