equal
deleted
inserted
replaced
74 \end{isamarkuptext}% |
74 \end{isamarkuptext}% |
75 \isacommand{lemma}\ wf{\isacharunderscore}id{\isacharcolon}\ {\isachardoublequote}wf\ r\ {\isasymLongrightarrow}\ wf{\isacharparenleft}id\ r{\isacharparenright}{\isachardoublequote}\isanewline |
75 \isacommand{lemma}\ wf{\isacharunderscore}id{\isacharcolon}\ {\isachardoublequote}wf\ r\ {\isasymLongrightarrow}\ wf{\isacharparenleft}id\ r{\isacharparenright}{\isachardoublequote}\isanewline |
76 \isacommand{by}\ simp% |
76 \isacommand{by}\ simp% |
77 \begin{isamarkuptext}% |
77 \begin{isamarkuptext}% |
78 \noindent |
78 \noindent |
79 and should have appended the following hint to our above definition: |
79 and should have appended the following hint to our definition above: |
80 \indexbold{*recdef_wf}% |
80 \indexbold{*recdef_wf}% |
81 \end{isamarkuptext}% |
81 \end{isamarkuptext}% |
82 {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}wf{\isacharcolon}\ wf{\isacharunderscore}id{\isacharparenright}\end{isabellebody}% |
82 {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}wf{\isacharcolon}\ wf{\isacharunderscore}id{\isacharparenright}\end{isabellebody}% |
83 %%% Local Variables: |
83 %%% Local Variables: |
84 %%% mode: latex |
84 %%% mode: latex |