1\DOC mk_state 2 3\TYPE {mk_state : term -> (string,term) list -> term} 4 5\SYNOPSIS 6Given the initial states and transition system of a HolCheck model, constructs a state tuple that can be used to specify HolCheck properites. 7 8\DESCRIBE 9HolCheck 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. 10 11\SEEALSO 12holCheckLib.holCheck, 13holCheckLib.set_state. 14 15\ENDDOC