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