equal
deleted
inserted
replaced
177 text {* |
177 text {* |
178 \noindent Note the occurrence of the name @{text mult_nat} in the |
178 \noindent Note the occurrence of the name @{text mult_nat} in the |
179 primrec declaration; by default, the local name of a class operation |
179 primrec declaration; by default, the local name of a class operation |
180 @{text f} to be instantiated on type constructor @{text \<kappa>} is |
180 @{text f} to be instantiated on type constructor @{text \<kappa>} is |
181 mangled as @{text f_\<kappa>}. In case of uncertainty, these names may be |
181 mangled as @{text f_\<kappa>}. In case of uncertainty, these names may be |
182 inspected using the @{command "print_context"} command or the |
182 inspected using the @{command "print_context"} command. |
183 corresponding ProofGeneral button. |
|
184 *} |
183 *} |
185 |
184 |
186 subsection {* Lifting and parametric types *} |
185 subsection {* Lifting and parametric types *} |
187 |
186 |
188 text {* |
187 text {* |