Lines Matching defs:about
533 relations (proof by extensionality), and rules about the empty set and the
680 rule \tdx{UnCI} is useful for classical reasoning about unions,
736 Reasoning directly about subsets often yields clearer proofs than
737 reasoning about the membership relation. Section~\ref{sec:ZF-pow-example}
930 about. The ZF theory provides many derived rules, which overlap more
1599 mechanisms for reasoning about freeness. The datatype package can handle both
1775 Most of the theorems about datatypes become part of the default simpset. You
2346 effective reasoniung about operational semantics.
2417 \item Theory \isa{Cardinal\_AC} uses AC to prove simplified theorems about
2497 \section{A proof about powersets}\label{sec:ZF-pow-example}
2498 To demonstrate high-level reasoning about subsets, let us prove the
2630 The theory \isa{ZF/equalities.thy} has many similar proofs. Reasoning about
2638 \section{Low-level reasoning about functions}
2640 and \isa{eta} support reasoning about functions in a
2652 Using \tdx{apply_equality}, we reduce the equality to reasoning about
2715 examples of reasoning about functions.