equal
deleted
inserted
replaced
1 % |
1 % |
2 \begin{isabellebody}% |
2 \begin{isabellebody}% |
3 \def\isabellecontext{Nested{\isadigit{2}}}% |
3 \def\isabellecontext{Nested{\isadigit{2}}}% |
|
4 \isamarkupfalse% |
4 % |
5 % |
5 \isadelimtheory |
6 \isadelimtheory |
6 % |
7 % |
7 \endisadelimtheory |
8 \endisadelimtheory |
8 % |
9 % |
9 \isatagtheory |
10 \isatagtheory |
10 \isamarkupfalse% |
|
11 % |
11 % |
12 \endisatagtheory |
12 \endisatagtheory |
13 {\isafoldtheory}% |
13 {\isafoldtheory}% |
14 % |
14 % |
15 \isadelimtheory |
15 \isadelimtheory |
30 {\isafoldproof}% |
30 {\isafoldproof}% |
31 % |
31 % |
32 \isadelimproof |
32 \isadelimproof |
33 % |
33 % |
34 \endisadelimproof |
34 \endisadelimproof |
35 \isamarkupfalse% |
|
36 % |
35 % |
37 \begin{isamarkuptext}% |
36 \begin{isamarkuptext}% |
38 \noindent |
37 \noindent |
39 By making this theorem a simplification rule, \isacommand{recdef} |
38 By making this theorem a simplification rule, \isacommand{recdef} |
40 applies it automatically and the definition of \isa{trev} |
39 applies it automatically and the definition of \isa{trev} |
114 into a situation where you need to supply \isacommand{recdef} with new |
113 into a situation where you need to supply \isacommand{recdef} with new |
115 congruence rules, you can append a hint after the end of |
114 congruence rules, you can append a hint after the end of |
116 the recursion equations:\cmmdx{hints}% |
115 the recursion equations:\cmmdx{hints}% |
117 \end{isamarkuptext}% |
116 \end{isamarkuptext}% |
118 \isamarkuptrue% |
117 \isamarkuptrue% |
119 \isamarkupfalse% |
|
120 \isamarkupfalse% |
|
121 {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}cong{\isacharcolon}\ map{\isacharunderscore}cong{\isacharparenright}% |
118 {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}cong{\isacharcolon}\ map{\isacharunderscore}cong{\isacharparenright}% |
122 \begin{isamarkuptext}% |
119 \begin{isamarkuptext}% |
123 \noindent |
120 \noindent |
124 Or you can declare them globally |
121 Or you can declare them globally |
125 by giving them the \attrdx{recdef_cong} attribute:% |
122 by giving them the \attrdx{recdef_cong} attribute:% |
140 \isadelimtheory |
137 \isadelimtheory |
141 % |
138 % |
142 \endisadelimtheory |
139 \endisadelimtheory |
143 % |
140 % |
144 \isatagtheory |
141 \isatagtheory |
145 \isamarkupfalse% |
|
146 % |
142 % |
147 \endisatagtheory |
143 \endisatagtheory |
148 {\isafoldtheory}% |
144 {\isafoldtheory}% |
149 % |
145 % |
150 \isadelimtheory |
146 \isadelimtheory |