equal
deleted
inserted
replaced
1 % |
1 % |
2 \begin{isabellebody}% |
2 \begin{isabellebody}% |
3 \def\isabellecontext{case{\isacharunderscore}exprs}% |
3 \def\isabellecontext{case{\isacharunderscore}exprs}% |
4 % |
4 % |
5 \isamarkupsubsection{Case expressions% |
5 \isamarkupsubsection{Case Expressions% |
6 } |
6 } |
7 % |
7 % |
8 \begin{isamarkuptext}% |
8 \begin{isamarkuptext}% |
9 \label{sec:case-expressions} |
9 \label{sec:case-expressions} |
10 HOL also features \isaindexbold{case}-expressions for analyzing |
10 HOL also features \isaindexbold{case}-expressions for analyzing |
47 |
47 |
48 Note that \isa{case}-expressions may need to be enclosed in parentheses to |
48 Note that \isa{case}-expressions may need to be enclosed in parentheses to |
49 indicate their scope% |
49 indicate their scope% |
50 \end{isamarkuptext}% |
50 \end{isamarkuptext}% |
51 % |
51 % |
52 \isamarkupsubsection{Structural induction and case distinction% |
52 \isamarkupsubsection{Structural Induction and Case Distinction% |
53 } |
53 } |
54 % |
54 % |
55 \begin{isamarkuptext}% |
55 \begin{isamarkuptext}% |
56 \label{sec:struct-ind-case} |
56 \label{sec:struct-ind-case} |
57 \indexbold{structural induction} |
57 \indexbold{structural induction} |