Lines Matching defs:example
61 that justify derived rules of definition. For example, recursive
81 The following is a simple but typical example of a relation defined inductively
82 by a set of rules. (This example is taken from~\cite{pitts}.) Let $R \subseteq
203 Consider, for example, the rules given above for reflexive-transitive closure.
227 simply by taking the intersection of all such relations. For example, a
260 illustrated by the {\sf Rtc} example given above. Such a definition, however,
268 In the case of the simple reflexive-transitive closure example, the first proof
369 \subsection{A simple example}
371 The following example {\small HOL} session shows how the function
399 The value supplied for the pattern in this example is the pair
404 of relations is being defined (see below). In this example,
459 An example of the role of the pattern argument in defining a class of relations
527 In addition to the use of the pattern argument, the \verb!Rtc! example also
596 \verb!Rtc!, for example, is:
641 \subsection{An example}
709 The proof sketched above is a trivial example of the kind of reasoning
713 theory (for example, operational semantics and process algebras), is made
736 Consider, for example, the theorem which states the transitivity rule for
769 {\small HOL} (i.e.\ to {\small ML} functions). For example, the transitivity
816 by \verb!derive_cases_thm! for the \verb!Rtc! example introduced above. The
857 In a joint project with Juanito Camilleri, a set of example proofs has