summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Sat, 10 Nov 2007 14:31:18 +0100 | |

changeset 25369 | 5200374fda5d |

parent 25368 | f12613fda79d |

child 25370 | 8b1aa4357320 |

replaced @{const} (allows name only) by proper @{term};

doc-src/IsarAdvanced/Classes/Thy/Classes.thy | file | annotate | diff | comparison | revisions | |

doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy | file | annotate | diff | comparison | revisions |

--- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy Fri Nov 09 23:24:31 2007 +0100 +++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy Sat Nov 10 14:31:18 2007 +0100 @@ -412,7 +412,7 @@ a canonical interpretation as type classes. Anyway, there is also the possibility of other interpretations. For example, also @{text "list"}s form a monoid with - @{const "op @"} and @{const "[]"} as operations, but it + @{term "op @"} and @{term "[]"} as operations, but it seems inappropriate to apply to lists the same operations as for genuinly algebraic types. In such a case, we simply can do a particular interpretation

--- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Fri Nov 09 23:24:31 2007 +0100 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Sat Nov 10 14:31:18 2007 +0100 @@ -471,7 +471,7 @@ @{text "Code_Integer"}. \item[@{text "Efficient_Nat"}] \label{eff_nat} implements natural numbers by integers, which in general will result in higher efficency; pattern - matching with @{const "0\<Colon>nat"} / @{const "Suc"} + matching with @{term "0\<Colon>nat"} / @{const "Suc"} is eliminated; includes @{text "Code_Integer"}. \item[@{text "Code_Index"}] provides an additional datatype @{text index} which is mapped to target-language built-in integers. @@ -548,13 +548,13 @@ theorems written in ML -- rewrite rules are generated dependent on the function theorems for a certain function. One application is the implicit expanding of @{typ nat} numerals - to @{const "0\<Colon>nat"} / @{const Suc} representation. See further + to @{term "0\<Colon>nat"} / @{const Suc} representation. See further \secref{sec:ml} \emph{Generic preprocessors} provide a most general interface, transforming a list of function theorems to another list of function theorems, provided that neither the heading - constant nor its type change. The @{const "0\<Colon>nat"} / @{const Suc} + constant nor its type change. The @{term "0\<Colon>nat"} / @{const Suc} pattern elimination implemented in theory @{text "EfficientNat"} (\secref{eff_nat}) uses this interface. @@ -646,7 +646,7 @@ text {* Then code generation will fail. Why? The definition - of @{const "op \<le>"} depends on equality on both arguments, + of @{term "op \<le>"} depends on equality on both arguments, which are polymorphic and impose an additional @{text eq} class constraint, thus violating the type discipline for class operations. @@ -740,7 +740,7 @@ text {* \noindent prints a table with \emph{all} defining equations - for @{const "op mod :: nat \<Rightarrow> nat \<Rightarrow> nat"}, including + for @{term "op mod :: nat \<Rightarrow> nat \<Rightarrow> nat"}, including \emph{all} defining equations those equations depend on recursivly. @{text "\<CODETHMS>"} provides a convenient mechanism to inspect the impact of a preprocessor setup @@ -1027,7 +1027,7 @@ text %mlref {* \begin{mldecls} - @{index_ML Code.add_func: "bool -> thm -> theory -> theory"} \\ + @{index_ML Code.add_func: "thm -> theory -> theory"} \\ @{index_ML Code.del_func: "thm -> theory -> theory"} \\ @{index_ML Code.add_funcl: "string * thm list Susp.T -> theory -> theory"} \\ @{index_ML Code.add_inline: "thm -> theory -> theory"} \\