--- a/NEWS Sun Feb 14 16:29:30 2016 +0100
+++ b/NEWS Sun Feb 14 16:30:27 2016 +0100
@@ -7,6 +7,10 @@
New in this Isabelle version
----------------------------
+*** Isar ***
+
+* Command '\<proof>' is an alias for 'sorry', with different
+typesetting. E.g. to produce proof holes in examples and documentation.
New in Isabelle2016 (February 2016)
--- a/lib/texinputs/isabellesym.sty Sun Feb 14 16:29:30 2016 +0100
+++ b/lib/texinputs/isabellesym.sty Sun Feb 14 16:30:27 2016 +0100
@@ -365,3 +365,4 @@
\newcommand{\isasymopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}
\newcommand{\isasymclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}
\newcommand{\isasymcomment}{\isatext{---}}
+\newcommand{\isasymproof}{\isamath{\,\langle\mathit{proof}\rangle}}
--- a/src/Doc/Isar_Ref/Base.thy Sun Feb 14 16:29:30 2016 +0100
+++ b/src/Doc/Isar_Ref/Base.thy Sun Feb 14 16:30:27 2016 +0100
@@ -2,14 +2,8 @@
theory Base
imports Pure
-keywords "\<proof>" :: "qed" % "proof"
begin
-ML \<open>
- Outer_Syntax.command @{command_keyword "\<proof>"} "dummy proof"
- (Scan.succeed Isar_Cmd.skip_proof);
-\<close>
-
ML_file "../antiquote_setup.ML"
end
--- a/src/Doc/Isar_Ref/document/style.sty Sun Feb 14 16:29:30 2016 +0100
+++ b/src/Doc/Isar_Ref/document/style.sty Sun Feb 14 16:30:27 2016 +0100
@@ -18,9 +18,6 @@
\newcommand{\isasymBBAR}{{\,\newdimen{\tmpheight}\settoheight\tmpheight{\isacharbar}\rule{1pt}{\tmpheight}\,}}
\renewcommand{\isacommand}[1]{\isakeyword{\isadigitreset#1}}
-\newcommand{\isasymproof}{\isamath{\,\langle\mathit{proof}\rangle}}
-
-
%% ML
\newenvironment{mldecls}{\par\noindent\begingroup\def\isanewline{\\}\begin{tabular}{ll}}{\end{tabular}\medskip\endgroup}
--- a/src/HOL/Imperative_HOL/document/root.tex Sun Feb 14 16:29:30 2016 +0100
+++ b/src/HOL/Imperative_HOL/document/root.tex Sun Feb 14 16:30:27 2016 +0100
@@ -55,9 +55,6 @@
\newcommand{\isactrlbvec}{\emph\bgroup\begin{math}{}\overline\bgroup\mbox\bgroup\isastylescript}
\newcommand{\isactrlevec}{\egroup\egroup\end{math}\egroup}
-% Isar proof
-\newcommand{\isasymproof}{$\;\langle\mathit{proof}\rangle$}
-
% Isar sorry
\renewcommand{\isacommand}[1]{\ifthenelse{\equal{sorry}{#1}}{\isasymproof}{\isakeyword{#1}}}
--- a/src/Pure/Isar/isar_syn.ML Sun Feb 14 16:29:30 2016 +0100
+++ b/src/Pure/Isar/isar_syn.ML Sun Feb 14 16:30:27 2016 +0100
@@ -669,6 +669,10 @@
(Scan.succeed Isar_Cmd.skip_proof);
val _ =
+ Outer_Syntax.command @{command_keyword "\<proof>"} "dummy proof (quick-and-dirty mode only!)"
+ (Scan.succeed Isar_Cmd.skip_proof);
+
+val _ =
Outer_Syntax.command @{command_keyword oops} "forget proof"
(Scan.succeed (Toplevel.forget_proof true));
--- a/src/Pure/Pure.thy Sun Feb 14 16:29:30 2016 +0100
+++ b/src/Pure/Pure.thy Sun Feb 14 16:30:27 2016 +0100
@@ -64,7 +64,7 @@
and "}" :: prf_close % "proof"
and "next" :: next_block % "proof"
and "qed" :: qed_block % "proof"
- and "by" ".." "." "sorry" :: "qed" % "proof"
+ and "by" ".." "." "sorry" "\<proof>" :: "qed" % "proof"
and "done" :: "qed_script" % "proof"
and "oops" :: qed_global % "proof"
and "defer" "prefer" "apply" :: prf_script % "proof"