diff -r 50d3059de9c6 -r 6e2479089226 ProgTutorial/First_Steps.thy --- a/ProgTutorial/First_Steps.thy Tue May 14 13:39:31 2019 +0200 +++ b/ProgTutorial/First_Steps.thy Tue May 14 16:59:53 2019 +0200 @@ -572,7 +572,7 @@ |-> (fn x => fn y => x + y)*} text {* - The combinator @{ML_ind ||>> in Basics} plays a central rôle whenever your + The combinator @{ML_ind ||>> in Basics} plays a central role whenever your task is to update a theory and the update also produces a side-result (for example a theorem). Functions for such tasks return a pair whose second component is the theory and the fist component is the side-result. Using