# HG changeset patch
# User nipkow
# Date 1150047370 -7200
# Node ID 600c35fd1b5ec107e19ecd5a4b49beba799905c7
# Parent  1704c66e5e7e0b8e8df0b38ba4f49ea64e5d7813
added quoting via back quotes

diff -r 1704c66e5e7e -r 600c35fd1b5e doc-src/IsarOverview/Isar/Logic.thy
--- a/doc-src/IsarOverview/Isar/Logic.thy	Sun Jun 11 00:42:22 2006 +0200
+++ b/doc-src/IsarOverview/Isar/Logic.thy	Sun Jun 11 19:36:10 2006 +0200
@@ -247,6 +247,7 @@
 \end{center}
 *}
 
+
 subsection{*Avoiding duplication*}
 
 text{* So far our examples have been a bit unnatural: normally we want to
@@ -346,6 +347,24 @@
   qed
 qed
 
+text{* Too many names can easily clutter a proof.  We already learned
+about @{text this} as a means of avoiding explicit names. Another
+handy device is to refer to a fact not by name but by contents: for
+example, writing @{text "`A \<or> B`"} (enclosing the formula in back quotes)
+refers to the fact @{text"A \<or> B"}
+without the need to name it. Here is a simple example, a revised version
+of the previous proof *}
+
+lemma assumes "A \<or> B" shows "B \<or> A"
+proof -
+  from `A \<or> B` show ?thesis
+(*<*)oops(*>*)
+text{*\noindent which continues as before.
+
+Clearly, this device of quoting facts by contents is only advisable
+for small formulae. In such cases it is superior to naming because the
+reader immediately sees what the fact is without needing to search for
+it in the preceding proof text. *}
 
 subsection{*Predicate calculus*}
 
@@ -415,14 +434,14 @@
   show "?S \<notin> range f"
   proof
     assume "?S \<in> range f"
-    then obtain y where fy: "?S = f y" ..
+    then obtain y where "?S = f y" ..
     show False
     proof cases
       assume "y \<in> ?S"
-      with fy show False by blast
+      with `?S = f y` show False by blast
     next
       assume "y \<notin> ?S"
-      with fy show False by blast
+      with `?S = f y` show False by blast
     qed
   qed
 qed
@@ -450,17 +469,17 @@
   show "?S \<notin> range f"
   proof
     assume "?S \<in> range f"
-    then obtain y where fy: "?S = f y" ..
+    then obtain y where "?S = f y" ..
     show False
     proof cases
       assume "y \<in> ?S"
       hence "y \<notin> f y"   by simp
-      hence "y \<notin> ?S"    by(simp add:fy)
+      hence "y \<notin> ?S"    by(simp add: `?S = f y`)
       thus False         by contradiction
     next
       assume "y \<notin> ?S"
       hence "y \<in> f y"   by simp
-      hence "y \<in> ?S"    by(simp add:fy)
+      hence "y \<in> ?S"    by(simp add: `?S = f y`)
       thus False         by contradiction
     qed
   qed
diff -r 1704c66e5e7e -r 600c35fd1b5e doc-src/IsarOverview/Isar/document/Logic.tex
--- a/doc-src/IsarOverview/Isar/document/Logic.tex	Sun Jun 11 00:42:22 2006 +0200
+++ b/doc-src/IsarOverview/Isar/document/Logic.tex	Sun Jun 11 19:36:10 2006 +0200
@@ -794,6 +794,46 @@
 %
 \endisadelimproof
 %
+\begin{isamarkuptext}%
+Too many names can easily clutter a proof.  We already learned
+about \isa{this} as a means of avoiding explicit names. Another
+handy device is to refer to a fact not by name but by contents: for
+example, writing \isa{{\isacharbackquote}A\ {\isasymor}\ B{\isacharbackquote}} (enclosing the formula in back quotes)
+refers to the fact \isa{A\ {\isasymor}\ B}
+without the need to name it. Here is a simple example, a revised version
+of the previous proof%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ \isakeyword{assumes}\ {\isachardoublequoteopen}A\ {\isasymor}\ B{\isachardoublequoteclose}\ \isakeyword{shows}\ {\isachardoublequoteopen}B\ {\isasymor}\ A{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{proof}\isamarkupfalse%
+\ {\isacharminus}\isanewline
+\ \ \isacommand{from}\isamarkupfalse%
+\ {\isacharbackquoteopen}A\ {\isasymor}\ B{\isacharbackquoteclose}\ \isacommand{show}\isamarkupfalse%
+\ {\isacharquery}thesis%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\noindent which continues as before.
+
+Clearly, this device of quoting facts by contents is only advisable
+for small formulae. In such cases it is superior to naming because the
+reader immediately sees what the fact is without needing to search for
+it in the preceding proof text.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
 \isamarkupsubsection{Predicate calculus%
 }
 \isamarkuptrue%
@@ -991,7 +1031,7 @@
 \ {\isachardoublequoteopen}{\isacharquery}S\ {\isasymin}\ range\ f{\isachardoublequoteclose}\isanewline
 \ \ \ \ \isacommand{then}\isamarkupfalse%
 \ \isacommand{obtain}\isamarkupfalse%
-\ y\ \isakeyword{where}\ fy{\isacharcolon}\ {\isachardoublequoteopen}{\isacharquery}S\ {\isacharequal}\ f\ y{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\ y\ \isakeyword{where}\ {\isachardoublequoteopen}{\isacharquery}S\ {\isacharequal}\ f\ y{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
 \isanewline
 \ \ \ \ \isacommand{show}\isamarkupfalse%
 \ False\isanewline
@@ -1000,7 +1040,7 @@
 \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
 \ {\isachardoublequoteopen}y\ {\isasymin}\ {\isacharquery}S{\isachardoublequoteclose}\isanewline
 \ \ \ \ \ \ \isacommand{with}\isamarkupfalse%
-\ fy\ \isacommand{show}\isamarkupfalse%
+\ {\isacharbackquoteopen}{\isacharquery}S\ {\isacharequal}\ f\ y{\isacharbackquoteclose}\ \isacommand{show}\isamarkupfalse%
 \ False\ \isacommand{by}\isamarkupfalse%
 \ blast\isanewline
 \ \ \ \ \isacommand{next}\isamarkupfalse%
@@ -1008,7 +1048,7 @@
 \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
 \ {\isachardoublequoteopen}y\ {\isasymnotin}\ {\isacharquery}S{\isachardoublequoteclose}\isanewline
 \ \ \ \ \ \ \isacommand{with}\isamarkupfalse%
-\ fy\ \isacommand{show}\isamarkupfalse%
+\ {\isacharbackquoteopen}{\isacharquery}S\ {\isacharequal}\ f\ y{\isacharbackquoteclose}\ \isacommand{show}\isamarkupfalse%
 \ False\ \isacommand{by}\isamarkupfalse%
 \ blast\isanewline
 \ \ \ \ \isacommand{qed}\isamarkupfalse%
@@ -1064,7 +1104,7 @@
 \ {\isachardoublequoteopen}{\isacharquery}S\ {\isasymin}\ range\ f{\isachardoublequoteclose}\isanewline
 \ \ \ \ \isacommand{then}\isamarkupfalse%
 \ \isacommand{obtain}\isamarkupfalse%
-\ y\ \isakeyword{where}\ fy{\isacharcolon}\ {\isachardoublequoteopen}{\isacharquery}S\ {\isacharequal}\ f\ y{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\ y\ \isakeyword{where}\ {\isachardoublequoteopen}{\isacharquery}S\ {\isacharequal}\ f\ y{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
 \isanewline
 \ \ \ \ \isacommand{show}\isamarkupfalse%
 \ False\isanewline
@@ -1077,7 +1117,7 @@
 \ simp\isanewline
 \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
 \ {\isachardoublequoteopen}y\ {\isasymnotin}\ {\isacharquery}S{\isachardoublequoteclose}\ \ \ \ \isacommand{by}\isamarkupfalse%
-{\isacharparenleft}simp\ add{\isacharcolon}fy{\isacharparenright}\isanewline
+{\isacharparenleft}simp\ add{\isacharcolon}\ {\isacharbackquoteopen}{\isacharquery}S\ {\isacharequal}\ f\ y{\isacharbackquoteclose}{\isacharparenright}\isanewline
 \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
 \ False\ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
 \ contradiction\isanewline
@@ -1090,7 +1130,7 @@
 \ simp\isanewline
 \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
 \ {\isachardoublequoteopen}y\ {\isasymin}\ {\isacharquery}S{\isachardoublequoteclose}\ \ \ \ \isacommand{by}\isamarkupfalse%
-{\isacharparenleft}simp\ add{\isacharcolon}fy{\isacharparenright}\isanewline
+{\isacharparenleft}simp\ add{\isacharcolon}\ {\isacharbackquoteopen}{\isacharquery}S\ {\isacharequal}\ f\ y{\isacharbackquoteclose}{\isacharparenright}\isanewline
 \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
 \ False\ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
 \ contradiction\isanewline