History log of /seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/ppc/ppc_opsemScript.sml
Revision Date Author Comments
# a2328149 23-Sep-2011 Anthony Fox <anthony.fox@cl.cam.ac.uk>

Adopt ML-style syntax for case expressions and use freed up "||" for bitwise-or. See issue #24.


# 845531b5 14-Sep-2011 Michael Norrish <Michael.Norrish@nicta.com.au>

Remove trailing whitespace in source files.


# 314727fa 01-Mar-2010 Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk>

Many minor changes.


# 4761143b 10-Aug-2009 Tjark Weber <Tjark.Weber@cl.cam.ac.uk>

Removed trailing whitespace from all .sml and .sig files.

This affects over 900 files and was done using emacs's delete-trailing-whitespace
function in batch mode. Building the system with Poly/ML and Moscow ML seems to
work, so I'm hoping these changes don't break anything. Please complain if
they do!


# 8c3fc760 09-Jun-2009 Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk>

A general update. Now lisp_finalTheory produces assembly files
containing the verified LISP interpeteres (in machine code):

arm_eval.s
x86_eval.s
ppc_eval.s

Each of these have been successfully run on real hardware, for
each respective platform.

The proof scripts are likely to only work in the experimental
kernel, due to some unfortuante differences between the two
kernels. Some of these differences are exposed more frequently
now due to recent(ish) changes to the datatype package. Maybe
some of the changes made to the datatype package ought to be
reconsidered?


# 44a6db21 03-Apr-2009 Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk>

Restructuring and simplification.


# 7c197d42 07-Jan-2009 Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk>

A new version of files previously in examples/mc-logic.
Eventually examples/mc-logic will be deleted.