# HG changeset patch
# User wenzelm
# Date 1234384683 -3600
# Node ID 0cfd533b4e37c478bb11ca7f91db04b74ec33643
# Parent  a06894e9b6e3eae528c2573ca2a9657b59d85367
tuned formal markup;

diff -r a06894e9b6e3 -r 0cfd533b4e37 doc-src/IsarRef/Thy/Proof.thy
--- a/doc-src/IsarRef/Thy/Proof.thy	Mon Feb 09 21:13:10 2009 +0100
+++ b/doc-src/IsarRef/Thy/Proof.thy	Wed Feb 11 21:38:03 2009 +0100
@@ -963,7 +963,7 @@
   \begin{matharray}{l}
     @{text "\<langle>using b\<^sub>1 \<dots> b\<^sub>k\<rangle>"}~~@{command "obtain"}~@{text "x\<^sub>1 \<dots> x\<^sub>m \<WHERE> a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n  \<langle>proof\<rangle> \<equiv>"} \\[1ex]
     \quad @{command "have"}~@{text "\<And>thesis. (\<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> thesis) \<Longrightarrow> thesis"} \\
-    \quad @{command "proof"}~@{text succeed} \\
+    \quad @{command "proof"}~@{method succeed} \\
     \qquad @{command "fix"}~@{text thesis} \\
     \qquad @{command "assume"}~@{text "that [Pure.intro?]: \<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> thesis"} \\
     \qquad @{command "then"}~@{command "show"}~@{text thesis} \\