Lines Matching refs:axioms
352 further specified using a set of axioms; for example, the class
354 order axioms. Of course, such axiomatizations are not possible in
371 satisfy the axioms of the class. Since our translation only generates
372 classes without axioms (beyond those of $pcpo$), proofs are trivial
1000 that satisfy the monadic axioms. This solution can be expressed in terms of
1002 signatures and axioms to theorems in ways that preserve operations and
1008 axioms, constants and type declarations. Building a theory morphism from
1019 respectively) and the relevant axioms (in \emph{MonadAxms}). To show that a
1024 the axioms. The following gives an example. \\
1103 \emph{Tx}, the user needs to prove the monad axioms as HOL lemmas (in this