src/Doc/Isar_Ref/Proof_Script.thy
changeset 61503 28e788ca2c5d
parent 61493 0debd22f0c0e
child 61656 cfabbc083977
     1.1 --- a/src/Doc/Isar_Ref/Proof_Script.thy	Thu Oct 22 21:16:27 2015 +0200
     1.2 +++ b/src/Doc/Isar_Ref/Proof_Script.thy	Thu Oct 22 21:16:49 2015 +0200
     1.3 @@ -111,7 +111,7 @@
     1.4    to them in the proof body: ``@{command subgoal}~@{keyword "for"}~\<open>x
     1.5    y z\<close>'' names a \<^emph>\<open>prefix\<close>, and ``@{command subgoal}~@{keyword
     1.6    "for"}~\<open>\<dots> x y z\<close>'' names a \<^emph>\<open>suffix\<close> of goal parameters. The
     1.7 -  latter uses a literal @{verbatim "\<dots>"} symbol as notation. Parameter
     1.8 +  latter uses a literal \<^verbatim>\<open>\<dots>\<close> symbol as notation. Parameter
     1.9    positions may be skipped via dummies (underscore). Unspecified names
    1.10    remain internal, and thus inaccessible in the proof text.
    1.11