# HG changeset patch
# User wenzelm
# Date 1455463827 -3600
# Node ID 5e5a881ebc128edda046aa25626e2dd8666a90da
# Parent  73bebf642d3ba65665fa0c2549c1428eb0437b26
command '\<proof>' is an alias for 'sorry', with different typesetting;

diff -r 73bebf642d3b -r 5e5a881ebc12 NEWS
--- 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)
diff -r 73bebf642d3b -r 5e5a881ebc12 lib/texinputs/isabellesym.sty
--- 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}}
diff -r 73bebf642d3b -r 5e5a881ebc12 src/Doc/Isar_Ref/Base.thy
--- 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
diff -r 73bebf642d3b -r 5e5a881ebc12 src/Doc/Isar_Ref/document/style.sty
--- 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}
 
diff -r 73bebf642d3b -r 5e5a881ebc12 src/HOL/Imperative_HOL/document/root.tex
--- 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}}}
 
diff -r 73bebf642d3b -r 5e5a881ebc12 src/Pure/Isar/isar_syn.ML
--- 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));
 
diff -r 73bebf642d3b -r 5e5a881ebc12 src/Pure/Pure.thy
--- 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"