--- a/src/Doc/Isar_Ref/First_Order_Logic.thy Sun Feb 07 19:33:42 2016 +0100
+++ b/src/Doc/Isar_Ref/First_Order_Logic.thy Sun Feb 07 19:43:40 2016 +0100
@@ -418,47 +418,47 @@
have "A \<longrightarrow> B"
proof
assume A
- show B sorry %noproof
+ show B \<proof>
qed
text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
- have "A \<longrightarrow> B" and A sorry %noproof
+ have "A \<longrightarrow> B" and A \<proof>
then have B ..
text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
- have A sorry %noproof
+ have A \<proof>
then have "A \<or> B" ..
- have B sorry %noproof
+ have B \<proof>
then have "A \<or> B" ..
text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
- have "A \<or> B" sorry %noproof
+ have "A \<or> B" \<proof>
then have C
proof
assume A
- then show C sorry %noproof
+ then show C \<proof>
next
assume B
- then show C sorry %noproof
+ then show C \<proof>
qed
text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
- have A and B sorry %noproof
+ have A and B \<proof>
then have "A \<and> B" ..
text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
- have "A \<and> B" sorry %noproof
+ have "A \<and> B" \<proof>
then obtain A and B ..
text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
- have "\<bottom>" sorry %noproof
+ have "\<bottom>" \<proof>
then have A ..
text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
@@ -470,12 +470,12 @@
have "\<not> A"
proof
assume A
- then show "\<bottom>" sorry %noproof
+ then show "\<bottom>" \<proof>
qed
text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
- have "\<not> A" and A sorry %noproof
+ have "\<not> A" and A \<proof>
then have B ..
text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
@@ -483,24 +483,24 @@
have "\<forall>x. B x"
proof
fix x
- show "B x" sorry %noproof
+ show "B x" \<proof>
qed
text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
- have "\<forall>x. B x" sorry %noproof
+ have "\<forall>x. B x" \<proof>
then have "B a" ..
text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
have "\<exists>x. B x"
proof
- show "B a" sorry %noproof
+ show "B a" \<proof>
qed
text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
- have "\<exists>x. B x" sorry %noproof
+ have "\<exists>x. B x" \<proof>
then obtain a where "B a" ..
text_raw \<open>\end{minipage}\<close>
--- a/src/Doc/Isar_Ref/Framework.thy Sun Feb 07 19:33:42 2016 +0100
+++ b/src/Doc/Isar_Ref/Framework.thy Sun Feb 07 19:43:40 2016 +0100
@@ -141,7 +141,7 @@
proof
fix A
assume "A \<in> \<A>"
- show "x \<in> A" sorry %noproof
+ show "x \<in> A" \<proof>
qed
(*<*)
end
@@ -192,7 +192,7 @@
proof
fix A
assume "x \<in> A" and "A \<in> \<A>"
- show C sorry %noproof
+ show C \<proof>
qed
(*<*)
end
@@ -664,25 +664,25 @@
text_raw \<open>\begin{minipage}[t]{0.45\textwidth}\<close>
{
fix x
- have "B x" sorry %noproof
+ have "B x" \<proof>
}
note \<open>\<And>x. B x\<close>
text_raw \<open>\end{minipage}\quad\begin{minipage}[t]{0.45\textwidth}\<close>(*<*)next(*>*)
{
assume A
- have B sorry %noproof
+ have B \<proof>
}
note \<open>A \<Longrightarrow> B\<close>
text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.45\textwidth}\<close>(*<*)next(*>*)
{
def x \<equiv> a
- have "B x" sorry %noproof
+ have "B x" \<proof>
}
note \<open>B a\<close>
text_raw \<open>\end{minipage}\quad\begin{minipage}[t]{0.45\textwidth}\<close>(*<*)next(*>*)
{
- obtain x where "A x" sorry %noproof
- have B sorry %noproof
+ obtain x where "A x" \<proof>
+ have B \<proof>
}
note \<open>B\<close>
text_raw \<open>\end{minipage}\<close>
@@ -754,7 +754,7 @@
shows "C x y"
proof -
from \<open>A x\<close> and \<open>B y\<close>
- show "C x y" sorry %noproof
+ show "C x y" \<proof>
qed
text_raw \<open>\end{minipage}\begin{minipage}{0.5\textwidth}\<close>
@@ -763,7 +763,7 @@
obtains x and y
where "A x" and "B y"
proof -
- have "A a" and "B b" sorry %noproof
+ have "A a" and "B b" \<proof>
then show thesis ..
qed
@@ -833,7 +833,7 @@
proof
assume A
show B
- sorry %noproof
+ \<proof>
qed
text_raw \<open>\end{minipage}\quad
\begin{minipage}[t]{0.06\textwidth}
@@ -892,7 +892,7 @@
proof -
fix x and y
assume "A x" and "B y"
- show "C x y" sorry %noproof
+ show "C x y" \<proof>
qed
text_raw \<open>\end{minipage}\begin{minipage}{0.5\textwidth}\<close>
@@ -904,7 +904,7 @@
proof -
fix x assume "A x"
fix y assume "B y"
- show "C x y" sorry %noproof
+ show "C x y" \<proof>
qed
text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}{0.5\textwidth}\<close>
@@ -916,7 +916,7 @@
proof -
fix y assume "B y"
fix x assume "A x"
- show "C x y" sorry
+ show "C x y" \<proof>
qed
text_raw \<open>\end{minipage}\begin{minipage}{0.5\textwidth}\<close>
@@ -927,7 +927,7 @@
proof -
fix y assume "B y"
fix x
- show "C x y" sorry
+ show "C x y" \<proof>
qed
(*<*)
end
@@ -1000,9 +1000,9 @@
notepad
begin
(*>*)
- have "a = b" sorry
- also have "\<dots> = c" sorry
- also have "\<dots> = d" sorry
+ have "a = b" \<proof>
+ also have "\<dots> = c" \<proof>
+ also have "\<dots> = d" \<proof>
finally have "a = d" .
(*<*)
end
--- a/src/Doc/Isar_Ref/Proof_Script.thy Sun Feb 07 19:33:42 2016 +0100
+++ b/src/Doc/Isar_Ref/Proof_Script.thy Sun Feb 07 19:43:40 2016 +0100
@@ -133,24 +133,24 @@
lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"
and "\<And>u v. X u \<Longrightarrow> Y v"
- subgoal sorry
- subgoal sorry
+ subgoal \<proof>
+ subgoal \<proof>
done
lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"
and "\<And>u v. X u \<Longrightarrow> Y v"
- subgoal for x y z sorry
- subgoal for u v sorry
+ subgoal for x y z \<proof>
+ subgoal for u v \<proof>
done
lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"
and "\<And>u v. X u \<Longrightarrow> Y v"
subgoal premises for x y z
using \<open>A x\<close> \<open>B y\<close>
- sorry
+ \<proof>
subgoal premises for u v
using \<open>X u\<close>
- sorry
+ \<proof>
done
lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"
@@ -159,21 +159,21 @@
proof -
have "A x" by (fact prems)
moreover have "B y" by (fact prems)
- ultimately show ?thesis sorry
+ ultimately show ?thesis \<proof>
qed
subgoal premises prems for u v
proof -
have "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z" by (fact r)
moreover
have "X u" by (fact prems)
- ultimately show ?thesis sorry
+ ultimately show ?thesis \<proof>
qed
done
lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"
subgoal premises prems for \<dots> z
proof -
- from prems show "C z" sorry
+ from prems show "C z" \<proof>
qed
done
--- a/src/Doc/Isar_Ref/Synopsis.thy Sun Feb 07 19:33:42 2016 +0100
+++ b/src/Doc/Isar_Ref/Synopsis.thy Sun Feb 07 19:43:40 2016 +0100
@@ -53,7 +53,7 @@
assume a: A
txt \<open>Via proof (``let''):\<close>
- have b: B sorry
+ have b: B \<proof>
txt \<open>Via abbreviation (``let''):\<close>
note c = a b
@@ -156,8 +156,8 @@
notepad
begin
{
- have a: A sorry
- have b: B sorry
+ have a: A \<proof>
+ have b: B \<proof>
note a b
}
note this
@@ -174,15 +174,15 @@
begin
{
- have a: A sorry
+ have a: A \<proof>
next
have b: B
proof -
- show B sorry
+ show B \<proof>
next
- have c: C sorry
+ have c: C \<proof>
next
- have d: D sorry
+ have d: D \<proof>
qed
}
@@ -190,19 +190,19 @@
{
{
- have a: A sorry
+ have a: A \<proof>
}
{
have b: B
proof -
{
- show B sorry
+ show B \<proof>
}
{
- have c: C sorry
+ have c: C \<proof>
}
{
- have d: D sorry
+ have d: D \<proof>
}
qed
}
@@ -235,7 +235,7 @@
have "x = y"
proof -
term ?thesis
- show ?thesis sorry
+ show ?thesis \<proof>
term ?thesis \<comment> \<open>static!\<close>
qed
term "\<dots>"
@@ -260,31 +260,31 @@
notepad
begin
txt \<open>Plain bottom-up calculation:\<close>
- have "a = b" sorry
+ have "a = b" \<proof>
also
- have "b = c" sorry
+ have "b = c" \<proof>
also
- have "c = d" sorry
+ have "c = d" \<proof>
finally
have "a = d" .
txt \<open>Variant using the \<open>\<dots>\<close> abbreviation:\<close>
- have "a = b" sorry
+ have "a = b" \<proof>
also
- have "\<dots> = c" sorry
+ have "\<dots> = c" \<proof>
also
- have "\<dots> = d" sorry
+ have "\<dots> = d" \<proof>
finally
have "a = d" .
txt \<open>Top-down version with explicit claim at the head:\<close>
have "a = d"
proof -
- have "a = b" sorry
+ have "a = b" \<proof>
also
- have "\<dots> = c" sorry
+ have "\<dots> = c" \<proof>
also
- have "\<dots> = d" sorry
+ have "\<dots> = d" \<proof>
finally
show ?thesis .
qed
@@ -292,11 +292,11 @@
txt \<open>Mixed inequalities (require suitable base type):\<close>
fix a b c d :: nat
- have "a < b" sorry
+ have "a < b" \<proof>
also
- have "b \<le> c" sorry
+ have "b \<le> c" \<proof>
also
- have "c = d" sorry
+ have "c = d" \<proof>
finally
have "a < d" .
end
@@ -321,31 +321,31 @@
notepad
begin
txt \<open>A vacuous proof:\<close>
- have A sorry
+ have A \<proof>
moreover
- have B sorry
+ have B \<proof>
moreover
- have C sorry
+ have C \<proof>
ultimately
have A and B and C .
next
txt \<open>Slightly more content (trivial bigstep reasoning):\<close>
- have A sorry
+ have A \<proof>
moreover
- have B sorry
+ have B \<proof>
moreover
- have C sorry
+ have C \<proof>
ultimately
have "A \<and> B \<and> C" by blast
next
txt \<open>More ambitious bigstep reasoning involving structured results:\<close>
- have "A \<or> B \<or> C" sorry
+ have "A \<or> B \<or> C" \<proof>
moreover
- { assume A have R sorry }
+ { assume A have R \<proof> }
moreover
- { assume B have R sorry }
+ { assume B have R \<proof> }
moreover
- { assume C have R sorry }
+ { assume C have R \<proof> }
ultimately
have R by blast \<comment> \<open>``big-bang integration'' of proof blocks (occasionally fragile)\<close>
end
@@ -367,11 +367,11 @@
fix n :: nat
have "P n"
proof (rule nat.induct) \<comment> \<open>fragile rule application!\<close>
- show "P 0" sorry
+ show "P 0" \<proof>
next
fix n :: nat
assume "P n"
- show "P (Suc n)" sorry
+ show "P (Suc n)" \<proof>
qed
end
@@ -394,10 +394,10 @@
have "P n"
proof (induct n)
case 0
- show ?case sorry
+ show ?case \<proof>
next
case (Suc n)
- from Suc.hyps show ?case sorry
+ from Suc.hyps show ?case \<proof>
qed
end
@@ -456,29 +456,29 @@
have "P n"
proof (induct n)
case 0
- show "P 0" sorry
+ show "P 0" \<proof>
next
case (Suc n)
- from \<open>P n\<close> show "P (Suc n)" sorry
+ from \<open>P n\<close> show "P (Suc n)" \<proof>
qed
have "A n \<Longrightarrow> P n"
proof (induct n)
case 0
- from \<open>A 0\<close> show "P 0" sorry
+ from \<open>A 0\<close> show "P 0" \<proof>
next
case (Suc n)
from \<open>A n \<Longrightarrow> P n\<close>
- and \<open>A (Suc n)\<close> show "P (Suc n)" sorry
+ and \<open>A (Suc n)\<close> show "P (Suc n)" \<proof>
qed
have "\<And>x. Q x n"
proof (induct n)
case 0
- show "Q x 0" sorry
+ show "Q x 0" \<proof>
next
case (Suc n)
- from \<open>\<And>x. Q x n\<close> show "Q x (Suc n)" sorry
+ from \<open>\<And>x. Q x n\<close> show "Q x (Suc n)" \<proof>
txt \<open>Local quantification admits arbitrary instances:\<close>
note \<open>Q a n\<close> and \<open>Q b n\<close>
qed
@@ -502,11 +502,11 @@
then have "Q x n"
proof (induct n arbitrary: x)
case 0
- from \<open>A x 0\<close> show "Q x 0" sorry
+ from \<open>A x 0\<close> show "Q x 0" \<proof>
next
case (Suc n)
from \<open>\<And>x. A x n \<Longrightarrow> Q x n\<close> \<comment> \<open>arbitrary instances can be produced here\<close>
- and \<open>A x (Suc n)\<close> show "Q x (Suc n)" sorry
+ and \<open>A x (Suc n)\<close> show "Q x (Suc n)" \<proof>
qed
end
@@ -532,13 +532,13 @@
case 0
note prem = \<open>A (a x)\<close>
and defn = \<open>0 = a x\<close>
- show "P (a x)" sorry
+ show "P (a x)" \<proof>
next
case (Suc n)
note hyp = \<open>\<And>x. n = a x \<Longrightarrow> A (a x) \<Longrightarrow> P (a x)\<close>
and prem = \<open>A (a x)\<close>
and defn = \<open>Suc n = a x\<close>
- show "P (a x)" sorry
+ show "P (a x)" \<proof>
qed
end
@@ -628,7 +628,7 @@
begin
{
fix x
- have "B x" sorry
+ have "B x" \<proof>
}
have "\<And>x. B x" by fact
@@ -636,7 +636,7 @@
{
assume A
- have B sorry
+ have B \<proof>
}
have "A \<Longrightarrow> B" by fact
@@ -644,15 +644,15 @@
{
def x \<equiv> t
- have "B x" sorry
+ have "B x" \<proof>
}
have "B t" by fact
next
{
- obtain x :: 'a where "B x" sorry
- have C sorry
+ obtain x :: 'a where "B x" \<proof>
+ have C \<proof>
}
have C by fact
@@ -703,7 +703,7 @@
proof -
fix x
assume "A x"
- show "B x" sorry
+ show "B x" \<proof>
qed
have "\<And>x. A x \<Longrightarrow> B x"
@@ -711,7 +711,7 @@
{
fix x
assume "A x"
- show "B x" sorry
+ show "B x" \<proof>
} \<comment> "implicit block structure made explicit"
note \<open>\<And>x. A x \<Longrightarrow> B x\<close>
\<comment> "side exit for the resulting rule"
@@ -730,36 +730,36 @@
begin
assume r1: "A \<Longrightarrow> B \<Longrightarrow> C" \<comment> \<open>simple rule (Horn clause)\<close>
- have A sorry \<comment> "prefix of facts via outer sub-proof"
+ have A \<proof> \<comment> "prefix of facts via outer sub-proof"
then have C
proof (rule r1)
- show B sorry \<comment> "remaining rule premises via inner sub-proof"
+ show B \<proof> \<comment> "remaining rule premises via inner sub-proof"
qed
have C
proof (rule r1)
- show A sorry
- show B sorry
+ show A \<proof>
+ show B \<proof>
qed
- have A and B sorry
+ have A and B \<proof>
then have C
proof (rule r1)
qed
- have A and B sorry
+ have A and B \<proof>
then have C by (rule r1)
next
assume r2: "A \<Longrightarrow> (\<And>x. B1 x \<Longrightarrow> B2 x) \<Longrightarrow> C" \<comment> \<open>nested rule\<close>
- have A sorry
+ have A \<proof>
then have C
proof (rule r2)
fix x
assume "B1 x"
- show "B2 x" sorry
+ show "B2 x" \<proof>
qed
txt \<open>The compound rule premise @{prop "\<And>x. B1 x \<Longrightarrow> B2 x"} is better
@@ -777,35 +777,35 @@
notepad
begin
- have "A \<longrightarrow> B" and A sorry
+ have "A \<longrightarrow> B" and A \<proof>
then have B ..
- have A sorry
+ have A \<proof>
then have "A \<or> B" ..
- have B sorry
+ have B \<proof>
then have "A \<or> B" ..
- have "A \<or> B" sorry
+ have "A \<or> B" \<proof>
then have C
proof
assume A
- then show C sorry
+ then show C \<proof>
next
assume B
- then show C sorry
+ then show C \<proof>
qed
- have A and B sorry
+ have A and B \<proof>
then have "A \<and> B" ..
- have "A \<and> B" sorry
+ have "A \<and> B" \<proof>
then have A ..
- have "A \<and> B" sorry
+ have "A \<and> B" \<proof>
then have B ..
- have False sorry
+ have False \<proof>
then have A ..
have True ..
@@ -813,36 +813,36 @@
have "\<not> A"
proof
assume A
- then show False sorry
+ then show False \<proof>
qed
- have "\<not> A" and A sorry
+ have "\<not> A" and A \<proof>
then have B ..
have "\<forall>x. P x"
proof
fix x
- show "P x" sorry
+ show "P x" \<proof>
qed
- have "\<forall>x. P x" sorry
+ have "\<forall>x. P x" \<proof>
then have "P a" ..
have "\<exists>x. P x"
proof
- show "P a" sorry
+ show "P a" \<proof>
qed
- have "\<exists>x. P x" sorry
+ have "\<exists>x. P x" \<proof>
then have C
proof
fix a
assume "P a"
- show C sorry
+ show C \<proof>
qed
txt \<open>Less awkward version using @{command obtain}:\<close>
- have "\<exists>x. P x" sorry
+ have "\<exists>x. P x" \<proof>
then obtain a where "P a" ..
end
@@ -853,32 +853,32 @@
begin
have "A \<and> B"
proof \<comment> \<open>two strictly isolated subproofs\<close>
- show A sorry
+ show A \<proof>
next
- show B sorry
+ show B \<proof>
qed
have "A \<and> B"
proof \<comment> \<open>one simultaneous sub-proof\<close>
- show A and B sorry
+ show A and B \<proof>
qed
have "A \<and> B"
proof \<comment> \<open>two subproofs in the same context\<close>
- show A sorry
- show B sorry
+ show A \<proof>
+ show B \<proof>
qed
have "A \<and> B"
proof \<comment> \<open>swapped order\<close>
- show B sorry
- show A sorry
+ show B \<proof>
+ show A \<proof>
qed
have "A \<and> B"
proof \<comment> \<open>sequential subproofs\<close>
- show A sorry
- show B using \<open>A\<close> sorry
+ show A \<proof>
+ show B using \<open>A\<close> \<proof>
qed
end
@@ -893,23 +893,23 @@
notepad
begin
- have "x \<in> A" and "x \<in> B" sorry
+ have "x \<in> A" and "x \<in> B" \<proof>
then have "x \<in> A \<inter> B" ..
- have "x \<in> A" sorry
+ have "x \<in> A" \<proof>
then have "x \<in> A \<union> B" ..
- have "x \<in> B" sorry
+ have "x \<in> B" \<proof>
then have "x \<in> A \<union> B" ..
- have "x \<in> A \<union> B" sorry
+ have "x \<in> A \<union> B" \<proof>
then have C
proof
assume "x \<in> A"
- then show C sorry
+ then show C \<proof>
next
assume "x \<in> B"
- then show C sorry
+ then show C \<proof>
qed
next
@@ -917,19 +917,19 @@
proof
fix a
assume "a \<in> A"
- show "x \<in> a" sorry
+ show "x \<in> a" \<proof>
qed
- have "x \<in> \<Inter>A" sorry
+ have "x \<in> \<Inter>A" \<proof>
then have "x \<in> a"
proof
- show "a \<in> A" sorry
+ show "a \<in> A" \<proof>
qed
- have "a \<in> A" and "x \<in> a" sorry
+ have "a \<in> A" and "x \<in> a" \<proof>
then have "x \<in> \<Union>A" ..
- have "x \<in> \<Union>A" sorry
+ have "x \<in> \<Union>A" \<proof>
then obtain a where "a \<in> A" and "x \<in> a" ..
end
@@ -965,16 +965,16 @@
(\<And>x y. B2 x y \<Longrightarrow> C2 x y \<Longrightarrow> R) \<Longrightarrow> (* case 2 *)
R (* main conclusion *)"
- have A1 and A2 sorry
+ have A1 and A2 \<proof>
then have R
proof (rule r)
fix x y
assume "B1 x y" and "C1 x y"
- show ?thesis sorry
+ show ?thesis \<proof>
next
fix x y
assume "B2 x y" and "C2 x y"
- show ?thesis sorry
+ show ?thesis \<proof>
qed
end
@@ -1007,7 +1007,7 @@
obtains
(case1) x y where "B1 x y" and "C1 x y"
| (case2) x y where "B2 x y" and "C2 x y"
- sorry
+ \<proof>
subsubsection \<open>Example\<close>
@@ -1024,10 +1024,10 @@
have C
proof (cases "x = y" rule: tertium_non_datur)
case T
- from \<open>x = y\<close> show ?thesis sorry
+ from \<open>x = y\<close> show ?thesis \<proof>
next
case F
- from \<open>x \<noteq> y\<close> show ?thesis sorry
+ from \<open>x \<noteq> y\<close> show ?thesis \<proof>
qed
end
@@ -1047,10 +1047,10 @@
have C
proof (cases x)
case Foo
- from \<open>x = Foo\<close> show ?thesis sorry
+ from \<open>x = Foo\<close> show ?thesis \<proof>
next
case (Bar a)
- from \<open>x = Bar a\<close> show ?thesis sorry
+ from \<open>x = Bar a\<close> show ?thesis \<proof>
qed
end
@@ -1065,13 +1065,13 @@
begin
fix B :: "'a \<Rightarrow> bool"
- obtain x where "B x" sorry
+ obtain x where "B x" \<proof>
note \<open>B x\<close>
txt \<open>Conclusions from this context may not mention @{term x} again!\<close>
{
- obtain x where "B x" sorry
- from \<open>B x\<close> have C sorry
+ obtain x where "B x" \<proof>
+ from \<open>B x\<close> have C \<proof>
}
note \<open>C\<close>
end
--- a/src/Doc/Isar_Ref/document/style.sty Sun Feb 07 19:33:42 2016 +0100
+++ b/src/Doc/Isar_Ref/document/style.sty Sun Feb 07 19:43:40 2016 +0100
@@ -16,7 +16,6 @@
%% Isar
\newcommand{\isasymBBAR}{{\,\newdimen{\tmpheight}\settoheight\tmpheight{\isacharbar}\rule{1pt}{\tmpheight}\,}}
-\isafoldtag{noproof}\def\isafoldnoproof{~\isafold{proof}}
\renewcommand{\isacommand}[1]{\isakeyword{\isadigitreset#1}}
\newcommand{\isasymproof}{\isamath{\,\langle\mathit{proof}\rangle}}