mk_state : term -> (string,term) list -> term
STRUCTURE
SYNOPSIS
Given the initial states and transition system of a HolCheck model, constructs a state tuple that can be used to specify HolCheck properites.
DESCRIPTION
HolCheck models atomic propositions in properties as functions on the state. Thus we need a representation of the state to specify properties. This function is used to create such a representative. Its return value is also passed to holCheckLib.set_state to ensure that the properties and the model use the same state tuple.
SEEALSO
HOL  Kananaskis-10