command '\<proof>' is an alias for 'sorry', with different typesetting;
authorwenzelm
Sun Feb 14 16:30:27 2016 +0100 (2016-02-14)
changeset 623125e5a881ebc12
parent 62311 73bebf642d3b
child 62313 aaeee16a56f5
command '\<proof>' is an alias for 'sorry', with different typesetting;
NEWS
lib/texinputs/isabellesym.sty
src/Doc/Isar_Ref/Base.thy
src/Doc/Isar_Ref/document/style.sty
src/HOL/Imperative_HOL/document/root.tex
src/Pure/Isar/isar_syn.ML
src/Pure/Pure.thy
     1.1 --- a/NEWS	Sun Feb 14 16:29:30 2016 +0100
     1.2 +++ b/NEWS	Sun Feb 14 16:30:27 2016 +0100
     1.3 @@ -7,6 +7,10 @@
     1.4  New in this Isabelle version
     1.5  ----------------------------
     1.6  
     1.7 +*** Isar ***
     1.8 +
     1.9 +* Command '\<proof>' is an alias for 'sorry', with different
    1.10 +typesetting. E.g. to produce proof holes in examples and documentation.
    1.11  
    1.12  
    1.13  New in Isabelle2016 (February 2016)
     2.1 --- a/lib/texinputs/isabellesym.sty	Sun Feb 14 16:29:30 2016 +0100
     2.2 +++ b/lib/texinputs/isabellesym.sty	Sun Feb 14 16:30:27 2016 +0100
     2.3 @@ -365,3 +365,4 @@
     2.4  \newcommand{\isasymopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}
     2.5  \newcommand{\isasymclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}
     2.6  \newcommand{\isasymcomment}{\isatext{---}}
     2.7 +\newcommand{\isasymproof}{\isamath{\,\langle\mathit{proof}\rangle}}
     3.1 --- a/src/Doc/Isar_Ref/Base.thy	Sun Feb 14 16:29:30 2016 +0100
     3.2 +++ b/src/Doc/Isar_Ref/Base.thy	Sun Feb 14 16:30:27 2016 +0100
     3.3 @@ -2,14 +2,8 @@
     3.4  
     3.5  theory Base
     3.6  imports Pure
     3.7 -keywords "\<proof>" :: "qed" % "proof"
     3.8  begin
     3.9  
    3.10 -ML \<open>
    3.11 -  Outer_Syntax.command @{command_keyword "\<proof>"} "dummy proof"
    3.12 -    (Scan.succeed Isar_Cmd.skip_proof);
    3.13 -\<close>
    3.14 -
    3.15  ML_file "../antiquote_setup.ML"
    3.16  
    3.17  end
     4.1 --- a/src/Doc/Isar_Ref/document/style.sty	Sun Feb 14 16:29:30 2016 +0100
     4.2 +++ b/src/Doc/Isar_Ref/document/style.sty	Sun Feb 14 16:30:27 2016 +0100
     4.3 @@ -18,9 +18,6 @@
     4.4  \newcommand{\isasymBBAR}{{\,\newdimen{\tmpheight}\settoheight\tmpheight{\isacharbar}\rule{1pt}{\tmpheight}\,}}
     4.5  \renewcommand{\isacommand}[1]{\isakeyword{\isadigitreset#1}}
     4.6  
     4.7 -\newcommand{\isasymproof}{\isamath{\,\langle\mathit{proof}\rangle}}
     4.8 -
     4.9 -
    4.10  %% ML
    4.11  \newenvironment{mldecls}{\par\noindent\begingroup\def\isanewline{\\}\begin{tabular}{ll}}{\end{tabular}\medskip\endgroup}
    4.12  
     5.1 --- a/src/HOL/Imperative_HOL/document/root.tex	Sun Feb 14 16:29:30 2016 +0100
     5.2 +++ b/src/HOL/Imperative_HOL/document/root.tex	Sun Feb 14 16:30:27 2016 +0100
     5.3 @@ -55,9 +55,6 @@
     5.4  \newcommand{\isactrlbvec}{\emph\bgroup\begin{math}{}\overline\bgroup\mbox\bgroup\isastylescript}
     5.5  \newcommand{\isactrlevec}{\egroup\egroup\end{math}\egroup}
     5.6  
     5.7 -% Isar proof
     5.8 -\newcommand{\isasymproof}{$\;\langle\mathit{proof}\rangle$}
     5.9 -
    5.10  % Isar sorry
    5.11  \renewcommand{\isacommand}[1]{\ifthenelse{\equal{sorry}{#1}}{\isasymproof}{\isakeyword{#1}}}
    5.12  
     6.1 --- a/src/Pure/Isar/isar_syn.ML	Sun Feb 14 16:29:30 2016 +0100
     6.2 +++ b/src/Pure/Isar/isar_syn.ML	Sun Feb 14 16:30:27 2016 +0100
     6.3 @@ -669,6 +669,10 @@
     6.4      (Scan.succeed Isar_Cmd.skip_proof);
     6.5  
     6.6  val _ =
     6.7 +  Outer_Syntax.command @{command_keyword "\<proof>"} "dummy proof (quick-and-dirty mode only!)"
     6.8 +    (Scan.succeed Isar_Cmd.skip_proof);
     6.9 +
    6.10 +val _ =
    6.11    Outer_Syntax.command @{command_keyword oops} "forget proof"
    6.12      (Scan.succeed (Toplevel.forget_proof true));
    6.13  
     7.1 --- a/src/Pure/Pure.thy	Sun Feb 14 16:29:30 2016 +0100
     7.2 +++ b/src/Pure/Pure.thy	Sun Feb 14 16:30:27 2016 +0100
     7.3 @@ -64,7 +64,7 @@
     7.4    and "}" :: prf_close % "proof"
     7.5    and "next" :: next_block % "proof"
     7.6    and "qed" :: qed_block % "proof"
     7.7 -  and "by" ".." "." "sorry" :: "qed" % "proof"
     7.8 +  and "by" ".." "." "sorry" "\<proof>" :: "qed" % "proof"
     7.9    and "done" :: "qed_script" % "proof"
    7.10    and "oops" :: qed_global % "proof"
    7.11    and "defer" "prefer" "apply" :: prf_script % "proof"