equal
deleted
inserted
replaced
15 |
15 |
16 subsection {* Program refinement *} |
16 subsection {* Program refinement *} |
17 |
17 |
18 text {* |
18 text {* |
19 Program refinement works by choosing appropriate code equations |
19 Program refinement works by choosing appropriate code equations |
20 explicitly (cf.~\label{sec:equations}); as example, we use Fibonacci |
20 explicitly (cf.~\secref{sec:equations}); as example, we use Fibonacci |
21 numbers: |
21 numbers: |
22 *} |
22 *} |
23 |
23 |
24 fun %quote fib :: "nat \<Rightarrow> nat" where |
24 fun %quote fib :: "nat \<Rightarrow> nat" where |
25 "fib 0 = 0" |
25 "fib 0 = 0" |