History log of /seL4-l4v-10.1.1/HOL4/examples/miller/useful/HurdUseful.sml
Revision Date Author Comments
# cad05a52 27-Mar-2018 Michael Norrish <Michael.Norrish@nicta.com.au>

Fix examples/miller


# 7b2db5fb 30-Jul-2012 Tarek <tarek@Tarek-Ubuntu.(none)>

Added extra theories to examples/miller.


# 474acc2b 09-Jul-2012 Michael Norrish <michael.norrish@nicta.com.au>

Reorganise files under examples/miller.

In particular, combine formalizeUseful, subTypeUseful and
ho_proverUseful into one HurdUseful that is in its own directory.
Also, put Know and Suff tactics into that library so that they don't
need to be repeatedly redefined at the head of the various Script
files.