History log of /seL4-l4v-10.1.1/HOL4/src/emit/extended_emitScript.sml
Revision Date Author Comments
# 19a4860d 31-Mar-2014 Michael Norrish <Michael.Norrish@nicta.com.au>

Fix flow-on bugs in EmitML from changing EmitTeX.
# 2769d1bd 03-Oct-2012 Ramana Kumar <ramana.kumar@gmail.com>

add more defs from state_transformer to extended_emit
# 9c0d09ca 11-Apr-2012 Anthony Fox <anthony.fox@cl.cam.ac.uk>

The wrong version of IS_EMPTY was being emitted.
# 7d11cca4 10-Apr-2012 Anthony Fox <anthony.fox@cl.cam.ac.uk>

The script files in src/emit have been restructured into two theories: basis_emit and extended_emit.

This will break uses of EmitML, but these can be easily fixed — see examples/ARM/v4/arm_emitScript.sml and examples/ARM/v7/eval/arm_emitScript.sml.