equal
deleted
inserted
replaced
887 \subsection{Executable code} |
887 \subsection{Executable code} |
888 |
888 |
889 Isabelle/Pure provides two generic frameworks to support code |
889 Isabelle/Pure provides two generic frameworks to support code |
890 generation from executable specifications. Isabelle/HOL |
890 generation from executable specifications. Isabelle/HOL |
891 instantiates these mechanisms in a |
891 instantiates these mechanisms in a |
892 way that is amenable to end-user applications |
892 way that is amenable to end-user applications. |
893 |
893 |
894 One framework generates code from both functional and |
894 One framework generates code from both functional and |
895 relational programs to SML. See |
895 relational programs to SML. See |
896 \cite{isabelle-HOL} for further information (this actually covers the |
896 \cite{isabelle-HOL} for further information (this actually covers the |
897 new-style theory format as well). |
897 new-style theory format as well). |