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]: