equal
deleted
inserted
replaced
1084 \item The derived record operations \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}make{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}fields{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}extend{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}truncate{\isaliteral{22}{\isachardoublequote}}} are \emph{not} |
1084 \item The derived record operations \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}make{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}fields{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}extend{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}truncate{\isaliteral{22}{\isachardoublequote}}} are \emph{not} |
1085 treated automatically, but usually need to be expanded by hand, |
1085 treated automatically, but usually need to be expanded by hand, |
1086 using the collective fact \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}defs{\isaliteral{22}{\isachardoublequote}}}. |
1086 using the collective fact \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}defs{\isaliteral{22}{\isachardoublequote}}}. |
1087 |
1087 |
1088 \end{enumerate}% |
1088 \end{enumerate}% |
|
1089 \end{isamarkuptext}% |
|
1090 \isamarkuptrue% |
|
1091 % |
|
1092 \isamarkupsubsubsection{Examples% |
|
1093 } |
|
1094 \isamarkuptrue% |
|
1095 % |
|
1096 \begin{isamarkuptext}% |
|
1097 See \verb|~~/src/HOL/ex/Records.thy|, for example.% |
1089 \end{isamarkuptext}% |
1098 \end{isamarkuptext}% |
1090 \isamarkuptrue% |
1099 \isamarkuptrue% |
1091 % |
1100 % |
1092 \isamarkupsection{Adhoc tuples% |
1101 \isamarkupsection{Adhoc tuples% |
1093 } |
1102 } |