equal
deleted
inserted
replaced
15 languages @{text SML} @{cite SML}, @{text OCaml} @{cite OCaml}, |
15 languages @{text SML} @{cite SML}, @{text OCaml} @{cite OCaml}, |
16 @{text Haskell} @{cite "haskell-revised-report"} and @{text Scala} |
16 @{text Haskell} @{cite "haskell-revised-report"} and @{text Scala} |
17 @{cite "scala-overview-tech-report"}. |
17 @{cite "scala-overview-tech-report"}. |
18 |
18 |
19 To profit from this tutorial, some familiarity and experience with |
19 To profit from this tutorial, some familiarity and experience with |
20 @{theory HOL} @{cite "isa-tutorial"} and its basic theories is assumed. |
20 Isabelle/HOL @{cite "isa-tutorial"} and its basic theories is assumed. |
21 \<close> |
21 \<close> |
22 |
22 |
23 |
23 |
24 subsection \<open>Code generation principle: shallow embedding \label{sec:principle}\<close> |
24 subsection \<open>Code generation principle: shallow embedding \label{sec:principle}\<close> |
25 |
25 |