History log of /seL4-l4v-10.1.1/HOL4/examples/unification/triangular/first-order/walkScript.sml
Revision Date Author Comments
# f24dd063 08-Jan-2015 Michael Norrish <michael.norrish@nicta.com.au>

Get unification example to build in light of 92317114


# a574fc44 10-Apr-2014 Michael Norrish <michael.norrish@nicta.com.au>

Rename implicational theorems in relation to make room for equivalences

This affects TC_CASES1 and TC_CASES2 that were hardly ever being used.
See the release notes change for more discussion.


# cccd6178 08-May-2013 Ramana Kumar <ramana.kumar@gmail.com>

prove collapse preserves wfs (in examples/unification/triangular)


# 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.


# c26105ad 14-Apr-2011 Ramana Kumar <ramana.kumar@gmail.com>

New examples: unification algorithms in accumulator-passing style