History log of /seL4-l4v-master/HOL4/src/1/thmpos_dtype.sml
Revision Date Author Comments
# 03829d89 06-Apr-2020 Michael Norrish <michael.norrish@data61.csiro.au>

Move the match_position datatype from mp_then to its own file

This type will be used in the API to the forthcoming resolve_then.
Separating it out into a _dtype.sml file also avoids having to repeat
the datatype definition in .sig and .sml file.