changeset 69597 | ff784d5a5bfb |
parent 67443 | 3abf6a722518 |
--- a/src/Doc/Tutorial/Rules/Basic.thy Sat Jan 05 17:00:43 2019 +0100 +++ b/src/Doc/Tutorial/Rules/Basic.thy Sat Jan 05 17:24:33 2019 +0100 @@ -371,7 +371,7 @@ @{subgoals[display,indent=0,margin=65]} applying @text{someI} automatically instantiates -@{term f} to @{term "\<lambda>x. SOME y. P x y"} +\<^term>\<open>f\<close> to \<^term>\<open>\<lambda>x. SOME y. P x y\<close> \<close> by (rule someI)