summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/ex/Execute_Choice.thy

changeset 61933 | cf58b5b794b2 |

parent 61343 | 5b5656a63bd6 |

child 64267 | b9a1486e79be |

--- a/src/HOL/ex/Execute_Choice.thy Sat Dec 26 15:44:14 2015 +0100 +++ b/src/HOL/ex/Execute_Choice.thy Sat Dec 26 15:59:27 2015 +0100 @@ -57,7 +57,7 @@ unfolding valuesum_def by transfer (simp add: setsum_diff) text \<open> - Given @{text valuesum_rec} as initial description, we stepwise refine it to something executable; + Given \<open>valuesum_rec\<close> as initial description, we stepwise refine it to something executable; first, we formally insert the constructor @{term Mapping} and split the one equation into two, where the second one provides the necessary context: \<close> @@ -72,7 +72,7 @@ As a side effect the precondition disappears (but note this has nothing to do with choice!). The first equation deals with the uncritical empty case and can already be used for code generation. - Using @{text valuesum_choice}, we are able to prove an executable version of @{term valuesum}: + Using \<open>valuesum_choice\<close>, we are able to prove an executable version of @{term valuesum}: \<close> lemma valuesum_rec_exec [code]: