# HG changeset patch
# User nipkow
# Date 1115051369 -7200
# Node ID 5f0c8a3f022654caa0a3a148e6cb72c63f460bfd
# Parent  f45296bb1485177c1575d3041737e4219e72314b
fixed setsum problem

diff -r f45296bb1485 -r 5f0c8a3f0226 doc-src/IsarOverview/Isar/Induction.thy
--- a/doc-src/IsarOverview/Isar/Induction.thy	Mon May 02 16:28:33 2005 +0200
+++ b/doc-src/IsarOverview/Isar/Induction.thy	Mon May 02 18:29:29 2005 +0200
@@ -77,13 +77,16 @@
 subsection{*Structural induction*}
 
 text{* We start with an inductive proof where both cases are proved automatically: *}
-lemma "2 * (\<Sum>i<n+1. i) = n*(n+1)"
+lemma "2 * (\<Sum>i::nat = 0..<n+1. i) = n*(n+1)"
 by (induct n, simp_all)
 
-text{*\noindent If we want to expose more of the structure of the
+text{*\noindent The constraint @{text"::nat"} is needed because all of
+the operations involved are overloaded.
+
+If we want to expose more of the structure of the
 proof, we can use pattern matching to avoid having to repeat the goal
 statement: *}
-lemma "2 * (\<Sum>i<n+1. i) = n*(n+1)" (is "?P n")
+lemma "2 * (\<Sum>i::nat = 0..<n+1. i) = n*(n+1)" (is "?P n")
 proof (induct n)
   show "?P 0" by simp
 next
@@ -94,7 +97,7 @@
 text{* \noindent We could refine this further to show more of the equational
 proof. Instead we explore the same avenue as for case distinctions:
 introducing context via the \isakeyword{case} command: *}
-lemma "2 * (\<Sum>i<n+1. i) = n*(n+1)"
+lemma "2 * (\<Sum>i::nat = 0..<n+1. i) = n*(n+1)"
 proof (induct n)
   case 0 show ?case by simp
 next
diff -r f45296bb1485 -r 5f0c8a3f0226 doc-src/IsarOverview/Isar/document/Induction.tex
--- a/doc-src/IsarOverview/Isar/document/Induction.tex	Mon May 02 16:28:33 2005 +0200
+++ b/doc-src/IsarOverview/Isar/document/Induction.tex	Mon May 02 18:29:29 2005 +0200
@@ -26,19 +26,15 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}{\isasymnot}\ A\ {\isasymor}\ A{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{proof}\ cases\isanewline
-\ \ \isamarkupfalse%
-\isacommand{assume}\ {\isachardoublequote}A{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{thus}\ {\isacharquery}thesis\ \isamarkupfalse%
-\isacommand{{\isachardot}{\isachardot}}\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{next}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{assume}\ {\isachardoublequote}{\isasymnot}\ A{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{thus}\ {\isacharquery}thesis\ \isamarkupfalse%
-\isacommand{{\isachardot}{\isachardot}}\isanewline
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent The two cases must come in this order because \isa{cases} merely abbreviates \isa{{\isacharparenleft}rule\ case{\isacharunderscore}split{\isacharunderscore}thm{\isacharparenright}} where
@@ -55,19 +51,15 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}{\isasymnot}\ A\ {\isasymor}\ A{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{proof}\ {\isacharparenleft}cases\ {\isachardoublequote}A{\isachardoublequote}{\isacharparenright}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{case}\ True\ \isamarkupfalse%
-\isacommand{thus}\ {\isacharquery}thesis\ \isamarkupfalse%
-\isacommand{{\isachardot}{\isachardot}}\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{next}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{case}\ False\ \isamarkupfalse%
-\isacommand{thus}\ {\isacharquery}thesis\ \isamarkupfalse%
-\isacommand{{\isachardot}{\isachardot}}\isanewline
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent which is like the previous proof but instantiates
@@ -84,19 +76,15 @@
 \isamarkupfalse%
 \isacommand{lemma}\ {\isachardoublequote}length{\isacharparenleft}tl\ xs{\isacharparenright}\ {\isacharequal}\ length\ xs\ {\isacharminus}\ {\isadigit{1}}{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{proof}\ {\isacharparenleft}cases\ xs{\isacharparenright}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{case}\ Nil\ \isamarkupfalse%
-\isacommand{thus}\ {\isacharquery}thesis\ \isamarkupfalse%
-\isacommand{by}\ simp\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{next}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{case}\ Cons\ \isamarkupfalse%
-\isacommand{thus}\ {\isacharquery}thesis\ \isamarkupfalse%
-\isacommand{by}\ simp\isanewline
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent Here `\isakeyword{case}~\isa{Nil}' abbreviates
@@ -127,32 +115,30 @@
 We start with an inductive proof where both cases are proved automatically:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharless}n{\isacharplus}{\isadigit{1}}{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline
+\isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharcolon}{\isacharcolon}nat\ {\isacharequal}\ {\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharplus}{\isadigit{1}}{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{by}\ {\isacharparenleft}induct\ n{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isamarkupfalse%
+\isamarkupfalse%
 %
 \begin{isamarkuptext}%
-\noindent If we want to expose more of the structure of the
+\noindent The constraint \isa{{\isacharcolon}{\isacharcolon}nat} is needed because all of
+the operations involved are overloaded.
+
+If we want to expose more of the structure of the
 proof, we can use pattern matching to avoid having to repeat the goal
 statement:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharless}n{\isacharplus}{\isadigit{1}}{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequote}{\isacharquery}P\ n{\isachardoublequote}{\isacharparenright}\isanewline
+\isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharcolon}{\isacharcolon}nat\ {\isacharequal}\ {\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharplus}{\isadigit{1}}{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequote}{\isacharquery}P\ n{\isachardoublequote}{\isacharparenright}\isanewline
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{proof}\ {\isacharparenleft}induct\ n{\isacharparenright}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{show}\ {\isachardoublequote}{\isacharquery}P\ {\isadigit{0}}{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{by}\ simp\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{next}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{fix}\ n\ \isamarkupfalse%
-\isacommand{assume}\ {\isachardoublequote}{\isacharquery}P\ n{\isachardoublequote}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{thus}\ {\isachardoublequote}{\isacharquery}P{\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{by}\ simp\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent We could refine this further to show more of the equational
@@ -160,21 +146,17 @@
 introducing context via the \isakeyword{case} command:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharless}n{\isacharplus}{\isadigit{1}}{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline
+\isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharcolon}{\isacharcolon}nat\ {\isacharequal}\ {\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharplus}{\isadigit{1}}{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{proof}\ {\isacharparenleft}induct\ n{\isacharparenright}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{case}\ {\isadigit{0}}\ \isamarkupfalse%
-\isacommand{show}\ {\isacharquery}case\ \isamarkupfalse%
-\isacommand{by}\ simp\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{next}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{case}\ Suc\ \isamarkupfalse%
-\isacommand{thus}\ {\isacharquery}case\ \isamarkupfalse%
-\isacommand{by}\ simp\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent The implicitly defined \isa{{\isacharquery}case} refers to the
@@ -189,19 +171,15 @@
 \isamarkuptrue%
 \isacommand{lemma}\ \isakeyword{fixes}\ n{\isacharcolon}{\isacharcolon}nat\ \isakeyword{shows}\ {\isachardoublequote}n\ {\isacharless}\ n{\isacharasterisk}n\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{proof}\ {\isacharparenleft}induct\ n{\isacharparenright}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{case}\ {\isadigit{0}}\ \isamarkupfalse%
-\isacommand{show}\ {\isacharquery}case\ \isamarkupfalse%
-\isacommand{by}\ simp\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{next}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{case}\ {\isacharparenleft}Suc\ i{\isacharparenright}\ \isamarkupfalse%
-\isacommand{thus}\ {\isachardoublequote}Suc\ i\ {\isacharless}\ Suc\ i\ {\isacharasterisk}\ Suc\ i\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{by}\ simp\isanewline
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent Of course we could again have written
@@ -233,56 +211,33 @@
 \isacommand{lemma}\ \isakeyword{assumes}\ A{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isasymAnd}n{\isachardot}\ {\isacharparenleft}{\isasymAnd}m{\isachardot}\ m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P\ m{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}{\isachardoublequote}\isanewline
 \ \ \isakeyword{shows}\ {\isachardoublequote}P{\isacharparenleft}n{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{proof}\ {\isacharparenleft}rule\ A{\isacharparenright}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{show}\ {\isachardoublequote}{\isasymAnd}m{\isachardot}\ m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P\ m{\isachardoublequote}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{proof}\ {\isacharparenleft}induct\ n{\isacharparenright}\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{case}\ {\isadigit{0}}\ \isamarkupfalse%
-\isacommand{thus}\ {\isacharquery}case\ \isamarkupfalse%
-\isacommand{by}\ simp\isanewline
-\ \ \isamarkupfalse%
-\isacommand{next}\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{case}\ {\isacharparenleft}Suc\ n{\isacharparenright}\ \ \ %
-\isamarkupcmt{\isakeyword{fix} \isa{m} \isakeyword{assume} \isa{Suc}: \isa{{\isacharbraceleft}{\isacharbackslash}isachardoublequote{\isacharbraceright}{\isacharquery}m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P\ {\isacharquery}m{\isacharbraceleft}{\isacharbackslash}isachardoublequote{\isacharbraceright}} \isa{{\isacharbraceleft}{\isacharbackslash}isachardoublequote{\isacharbraceright}m\ {\isacharless}\ Suc\ n{\isacharbraceleft}{\isacharbackslash}isachardoublequote{\isacharbraceright}}%
-}
-\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{show}\ {\isacharquery}case\ \ \ \ %
-\isamarkupcmt{\isa{P\ m}%
-}
-\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{proof}\ cases\isanewline
-\ \ \ \ \ \ \isamarkupfalse%
-\isacommand{assume}\ eq{\isacharcolon}\ {\isachardoublequote}m\ {\isacharequal}\ n{\isachardoublequote}\isanewline
-\ \ \ \ \ \ \isamarkupfalse%
-\isacommand{from}\ Suc\ \isakeyword{and}\ A\ \isamarkupfalse%
-\isacommand{have}\ {\isachardoublequote}P\ n{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{by}\ blast\isanewline
-\ \ \ \ \ \ \isamarkupfalse%
-\isacommand{with}\ eq\ \isamarkupfalse%
-\isacommand{show}\ {\isachardoublequote}P\ m{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{by}\ simp\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{next}\isanewline
-\ \ \ \ \ \ \isamarkupfalse%
-\isacommand{assume}\ {\isachardoublequote}m\ {\isasymnoteq}\ n{\isachardoublequote}\isanewline
-\ \ \ \ \ \ \isamarkupfalse%
-\isacommand{with}\ Suc\ \isamarkupfalse%
-\isacommand{have}\ {\isachardoublequote}m\ {\isacharless}\ n{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{by}\ arith\isanewline
-\ \ \ \ \ \ \isamarkupfalse%
-\isacommand{thus}\ {\isachardoublequote}P\ m{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{by}{\isacharparenleft}rule\ Suc{\isacharparenright}\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{qed}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{qed}\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent Given the explanations above and the comments in the
@@ -329,21 +284,16 @@
 \isamarkuptrue%
 \isacommand{lemma}\ \isakeyword{assumes}\ A{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\ \isakeyword{shows}\ {\isachardoublequote}{\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{using}\ A\isanewline
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{proof}\ induct\isanewline
-\ \ \isamarkupfalse%
-\isacommand{case}\ refl\ \isamarkupfalse%
-\isacommand{thus}\ {\isacharquery}case\ \isamarkupfalse%
-\isacommand{{\isachardot}}\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{next}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{case}\ step\ \isamarkupfalse%
-\isacommand{thus}\ {\isacharquery}case\ \isamarkupfalse%
-\isacommand{by}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isachardot}step{\isacharparenright}\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent Rule induction is triggered by a fact $(x_1,\dots,x_n)
@@ -358,37 +308,22 @@
 \isacommand{lemma}\ \isakeyword{assumes}\ A{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\ \isakeyword{and}\ B{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline
 \ \ \isakeyword{shows}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{proof}\ {\isacharminus}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{from}\ A\ B\ \isamarkupfalse%
-\isacommand{show}\ {\isacharquery}thesis\isanewline
-\ \ \isamarkupfalse%
-\isacommand{proof}\ induct\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{fix}\ x\ \isamarkupfalse%
-\isacommand{assume}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\ \ %
-\isamarkupcmt{\isa{B}[\isa{y} := \isa{x}]%
-}
-\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{thus}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{{\isachardot}}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{next}\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{fix}\ x{\isacharprime}\ x\ y\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{assume}\ {\isadigit{1}}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x{\isacharprime}{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ r{\isachardoublequote}\ \isakeyword{and}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ IH{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\ \isakeyword{and}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ B{\isacharcolon}\ \ {\isachardoublequote}{\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{from}\ {\isadigit{1}}\ IH{\isacharbrackleft}OF\ B{\isacharbrackright}\ \isamarkupfalse%
-\isacommand{show}\ {\isachardoublequote}{\isacharparenleft}x{\isacharprime}{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{by}{\isacharparenleft}rule\ rtc{\isachardot}step{\isacharparenright}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{qed}\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent We start the proof with \isakeyword{from}~\isa{A\ B}. Only \isa{A} is ``consumed'' by the induction step.
@@ -446,38 +381,28 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ rot\ xs\ {\isacharequal}\ tl\ xs\ {\isacharat}\ {\isacharbrackleft}hd\ xs{\isacharbrackright}{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{proof}\ {\isacharparenleft}induct\ xs\ rule{\isacharcolon}\ rot{\isachardot}induct{\isacharparenright}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{case}\ {\isadigit{1}}\ \isamarkupfalse%
-\isacommand{thus}\ {\isacharquery}case\ \isamarkupfalse%
-\isacommand{by}\ simp\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{next}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{case}\ {\isadigit{2}}\ \isamarkupfalse%
-\isacommand{show}\ {\isacharquery}case\ \isamarkupfalse%
-\isacommand{by}\ simp\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{next}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{case}\ {\isacharparenleft}{\isadigit{3}}\ a\ b\ cs{\isacharparenright}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{have}\ {\isachardoublequote}rot\ {\isacharparenleft}a\ {\isacharhash}\ b\ {\isacharhash}\ cs{\isacharparenright}\ {\isacharequal}\ b\ {\isacharhash}\ rot{\isacharparenleft}a\ {\isacharhash}\ cs{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{by}\ simp\isanewline
-\ \ \isamarkupfalse%
-\isacommand{also}\ \isamarkupfalse%
-\isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isacharequal}\ b\ {\isacharhash}\ tl{\isacharparenleft}a\ {\isacharhash}\ cs{\isacharparenright}\ {\isacharat}\ {\isacharbrackleft}hd{\isacharparenleft}a\ {\isacharhash}\ cs{\isacharparenright}{\isacharbrackright}{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}{\isadigit{3}}{\isacharparenright}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{also}\ \isamarkupfalse%
-\isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isacharequal}\ tl\ {\isacharparenleft}a\ {\isacharhash}\ b\ {\isacharhash}\ cs{\isacharparenright}\ {\isacharat}\ {\isacharbrackleft}hd\ {\isacharparenleft}a\ {\isacharhash}\ b\ {\isacharhash}\ cs{\isacharparenright}{\isacharbrackright}{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{by}\ simp\isanewline
-\ \ \isamarkupfalse%
-\isacommand{finally}\ \isamarkupfalse%
-\isacommand{show}\ {\isacharquery}case\ \isamarkupfalse%
-\isacommand{{\isachardot}}\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent
@@ -495,7 +420,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isamarkupfalse%
-\isacommand{by}\ {\isacharparenleft}induct\ xs\ rule{\isacharcolon}\ rot{\isachardot}induct{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline
+\isanewline
 \isamarkupfalse%
 \isamarkupfalse%
 \end{isabellebody}%
diff -r f45296bb1485 -r 5f0c8a3f0226 doc-src/IsarOverview/Isar/document/Logic.tex
--- a/doc-src/IsarOverview/Isar/document/Logic.tex	Mon May 02 16:28:33 2005 +0200
+++ b/doc-src/IsarOverview/Isar/document/Logic.tex	Mon May 02 18:29:29 2005 +0200
@@ -22,14 +22,11 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ A{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{proof}\ {\isacharparenleft}rule\ impI{\isacharparenright}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{assume}\ a{\isacharcolon}\ {\isachardoublequote}A{\isachardoublequote}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{show}\ {\isachardoublequote}A{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{by}{\isacharparenleft}rule\ a{\isacharparenright}\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent
@@ -45,14 +42,11 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ A{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{proof}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{assume}\ a{\isacharcolon}\ A\isanewline
-\ \ \isamarkupfalse%
-\isacommand{show}\ A\ \isamarkupfalse%
-\isacommand{by}{\isacharparenleft}rule\ a{\isacharparenright}\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent Single-identifier formulae such as \isa{A} need not
@@ -66,14 +60,11 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ A{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{proof}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{assume}\ {\isachardoublequote}A{\isachardoublequote}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{show}\ {\isachardoublequote}A{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{{\isachardot}}\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 To hide proofs by assumption further, \isakeyword{by}\isa{{\isacharparenleft}method{\isacharparenright}}
@@ -83,14 +74,11 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ A\ {\isasymand}\ A{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{proof}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{assume}\ {\isachardoublequote}A{\isachardoublequote}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{show}\ {\isachardoublequote}A\ {\isasymand}\ A{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{by}{\isacharparenleft}rule\ conjI{\isacharparenright}\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent Rule \isa{conjI} is of course \isa{{\isasymlbrakk}{\isacharquery}P{\isacharsemicolon}\ {\isacharquery}Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P\ {\isasymand}\ {\isacharquery}Q}.
@@ -104,14 +92,11 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ A\ {\isasymand}\ A{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{proof}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{assume}\ {\isachardoublequote}A{\isachardoublequote}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{show}\ {\isachardoublequote}A\ {\isasymand}\ A{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{{\isachardot}{\isachardot}}\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent
@@ -136,25 +121,15 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymand}\ B\ {\isasymlongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{proof}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{assume}\ AB{\isacharcolon}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{show}\ {\isachardoublequote}B\ {\isasymand}\ A{\isachardoublequote}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{proof}\ {\isacharparenleft}rule\ conjE{\isacharbrackleft}OF\ AB{\isacharbrackright}{\isacharparenright}\ \ %
-\isamarkupcmt{\isa{conjE{\isacharbrackleft}OF\ AB{\isacharbrackright}}: \isa{{\isacharparenleft}{\isasymlbrakk}A{\isacharsemicolon}\ B{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}R{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharquery}R}%
-}
-\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{assume}\ {\isachardoublequote}A{\isachardoublequote}\ {\isachardoublequote}B{\isachardoublequote}\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
-\isacommand{{\isachardot}{\isachardot}}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{qed}\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent Note that the term \isa{{\isacharquery}thesis} always stands for the
@@ -180,23 +155,16 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymand}\ B\ {\isasymlongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{proof}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{assume}\ AB{\isacharcolon}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{from}\ AB\ \isamarkupfalse%
-\isacommand{show}\ {\isachardoublequote}B\ {\isasymand}\ A{\isachardoublequote}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{proof}\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{assume}\ {\isachardoublequote}A{\isachardoublequote}\ {\isachardoublequote}B{\isachardoublequote}\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
-\isacommand{{\isachardot}{\isachardot}}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{qed}\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 Now we come to a second important principle:
@@ -210,23 +178,16 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymand}\ B\ {\isasymlongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{proof}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{assume}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{from}\ this\ \isamarkupfalse%
-\isacommand{show}\ {\isachardoublequote}B\ {\isasymand}\ A{\isachardoublequote}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{proof}\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{assume}\ {\isachardoublequote}A{\isachardoublequote}\ {\isachardoublequote}B{\isachardoublequote}\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
-\isacommand{{\isachardot}{\isachardot}}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{qed}\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent Because of the frequency of \isakeyword{from}~\isa{this}, Isar provides two abbreviations:
@@ -242,23 +203,18 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymand}\ B\ {\isasymlongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{proof}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{assume}\ ab{\isacharcolon}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{from}\ ab\ \isamarkupfalse%
-\isacommand{have}\ a{\isacharcolon}\ {\isachardoublequote}A{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{{\isachardot}{\isachardot}}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{from}\ ab\ \isamarkupfalse%
-\isacommand{have}\ b{\isacharcolon}\ {\isachardoublequote}B{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{{\isachardot}{\isachardot}}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{from}\ b\ a\ \isamarkupfalse%
-\isacommand{show}\ {\isachardoublequote}B\ {\isasymand}\ A{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{{\isachardot}{\isachardot}}\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent It is worth examining this text in detail because it
@@ -309,25 +265,19 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymand}\ B\ {\isasymlongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{proof}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{assume}\ ab{\isacharcolon}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{from}\ ab\ \isamarkupfalse%
-\isacommand{have}\ {\isachardoublequote}B{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{{\isachardot}{\isachardot}}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{moreover}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{from}\ ab\ \isamarkupfalse%
-\isacommand{have}\ {\isachardoublequote}A{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{{\isachardot}{\isachardot}}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{ultimately}\ \isamarkupfalse%
-\isacommand{show}\ {\isachardoublequote}B\ {\isasymand}\ A{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{{\isachardot}{\isachardot}}\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent You can combine any number of facts \isa{A{\isadigit{1}}} \dots\ \isa{An} into a sequence by separating their proofs with
@@ -346,56 +296,36 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}{\isasymnot}\ {\isacharparenleft}A\ {\isasymand}\ B{\isacharparenright}\ {\isasymlongrightarrow}\ {\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ B{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{proof}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{assume}\ n{\isacharcolon}\ {\isachardoublequote}{\isasymnot}\ {\isacharparenleft}A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{show}\ {\isachardoublequote}{\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ B{\isachardoublequote}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{proof}\ {\isacharparenleft}rule\ ccontr{\isacharparenright}\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{assume}\ nn{\isacharcolon}\ {\isachardoublequote}{\isasymnot}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ B{\isacharparenright}{\isachardoublequote}\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{have}\ {\isachardoublequote}{\isasymnot}\ A{\isachardoublequote}\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{proof}\isanewline
-\ \ \ \ \ \ \isamarkupfalse%
-\isacommand{assume}\ {\isachardoublequote}A{\isachardoublequote}\isanewline
-\ \ \ \ \ \ \isamarkupfalse%
-\isacommand{have}\ {\isachardoublequote}{\isasymnot}\ B{\isachardoublequote}\isanewline
-\ \ \ \ \ \ \isamarkupfalse%
-\isacommand{proof}\isanewline
-\ \ \ \ \ \ \ \ \isamarkupfalse%
-\isacommand{assume}\ {\isachardoublequote}B{\isachardoublequote}\isanewline
-\ \ \ \ \ \ \ \ \isamarkupfalse%
-\isacommand{have}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{{\isachardot}{\isachardot}}\isanewline
-\ \ \ \ \ \ \ \ \isamarkupfalse%
-\isacommand{with}\ n\ \isamarkupfalse%
-\isacommand{show}\ False\ \isamarkupfalse%
-\isacommand{{\isachardot}{\isachardot}}\isanewline
-\ \ \ \ \ \ \isamarkupfalse%
-\isacommand{qed}\isanewline
-\ \ \ \ \ \ \isamarkupfalse%
-\isacommand{hence}\ {\isachardoublequote}{\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ B{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{{\isachardot}{\isachardot}}\isanewline
-\ \ \ \ \ \ \isamarkupfalse%
-\isacommand{with}\ nn\ \isamarkupfalse%
-\isacommand{show}\ False\ \isamarkupfalse%
-\isacommand{{\isachardot}{\isachardot}}\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{qed}\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{hence}\ {\isachardoublequote}{\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ B{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{{\isachardot}{\isachardot}}\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{with}\ nn\ \isamarkupfalse%
-\isacommand{show}\ False\ \isamarkupfalse%
-\isacommand{{\isachardot}{\isachardot}}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{qed}\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent
@@ -425,19 +355,15 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymand}\ B\ {\isasymLongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{proof}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{assume}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{thus}\ {\isachardoublequote}B{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{{\isachardot}{\isachardot}}\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{next}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{assume}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{thus}\ {\isachardoublequote}A{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{{\isachardot}{\isachardot}}\isanewline
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent The \isakeyword{proof} always works on the conclusion,
@@ -468,19 +394,15 @@
 \isacommand{lemma}\ {\isachardoublequote}large{\isacharunderscore}A\ {\isasymand}\ large{\isacharunderscore}B\ {\isasymLongrightarrow}\ large{\isacharunderscore}B\ {\isasymand}\ large{\isacharunderscore}A{\isachardoublequote}\isanewline
 \ \ \ \ \ \ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequote}{\isacharquery}AB\ {\isasymLongrightarrow}\ {\isacharquery}B\ {\isasymand}\ {\isacharquery}A{\isachardoublequote}{\isacharparenright}\isanewline
 \isamarkupfalse%
-\isacommand{proof}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{assume}\ {\isachardoublequote}{\isacharquery}AB{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{thus}\ {\isachardoublequote}{\isacharquery}B{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{{\isachardot}{\isachardot}}\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{next}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{assume}\ {\isachardoublequote}{\isacharquery}AB{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{thus}\ {\isachardoublequote}{\isacharquery}A{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{{\isachardot}{\isachardot}}\isanewline
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent Any formula may be followed by
@@ -497,19 +419,15 @@
 \isacommand{lemma}\ \isakeyword{assumes}\ AB{\isacharcolon}\ {\isachardoublequote}large{\isacharunderscore}A\ {\isasymand}\ large{\isacharunderscore}B{\isachardoublequote}\isanewline
 \ \ \isakeyword{shows}\ {\isachardoublequote}large{\isacharunderscore}B\ {\isasymand}\ large{\isacharunderscore}A{\isachardoublequote}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequote}{\isacharquery}B\ {\isasymand}\ {\isacharquery}A{\isachardoublequote}{\isacharparenright}\isanewline
 \isamarkupfalse%
-\isacommand{proof}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{from}\ AB\ \isamarkupfalse%
-\isacommand{show}\ {\isachardoublequote}{\isacharquery}B{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{{\isachardot}{\isachardot}}\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{next}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{from}\ AB\ \isamarkupfalse%
-\isacommand{show}\ {\isachardoublequote}{\isacharquery}A{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{{\isachardot}{\isachardot}}\isanewline
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent Note the difference between \isa{{\isacharquery}AB}, a term, and
@@ -523,15 +441,12 @@
 \isacommand{lemma}\ \isakeyword{assumes}\ AB{\isacharcolon}\ {\isachardoublequote}large{\isacharunderscore}A\ {\isasymand}\ large{\isacharunderscore}B{\isachardoublequote}\isanewline
 \ \ \isakeyword{shows}\ {\isachardoublequote}large{\isacharunderscore}B\ {\isasymand}\ large{\isacharunderscore}A{\isachardoublequote}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequote}{\isacharquery}B\ {\isasymand}\ {\isacharquery}A{\isachardoublequote}{\isacharparenright}\isanewline
 \isamarkupfalse%
-\isacommand{using}\ AB\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{proof}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{assume}\ {\isachardoublequote}{\isacharquery}A{\isachardoublequote}\ {\isachardoublequote}{\isacharquery}B{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
-\isacommand{{\isachardot}{\isachardot}}\isanewline
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent Command \isakeyword{using} can appear before a proof
@@ -553,26 +468,19 @@
 \isamarkuptrue%
 \isacommand{lemma}\ \isakeyword{assumes}\ AB{\isacharcolon}\ {\isachardoublequote}A\ {\isasymor}\ B{\isachardoublequote}\ \isakeyword{shows}\ {\isachardoublequote}B\ {\isasymor}\ A{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{proof}\ {\isacharminus}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{from}\ AB\ \isamarkupfalse%
-\isacommand{show}\ {\isacharquery}thesis\isanewline
-\ \ \isamarkupfalse%
-\isacommand{proof}\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{assume}\ A\ \isamarkupfalse%
-\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
-\isacommand{{\isachardot}{\isachardot}}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{next}\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{assume}\ B\ \isamarkupfalse%
-\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
-\isacommand{{\isachardot}{\isachardot}}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{qed}\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 %
 \isamarkupsubsection{Predicate calculus%
 }
@@ -589,21 +497,12 @@
 \isamarkuptrue%
 \isacommand{lemma}\ \isakeyword{assumes}\ P{\isacharcolon}\ {\isachardoublequote}{\isasymforall}x{\isachardot}\ P\ x{\isachardoublequote}\ \isakeyword{shows}\ {\isachardoublequote}{\isasymforall}x{\isachardot}\ P{\isacharparenleft}f\ x{\isacharparenright}{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{proof}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ %
-\isamarkupcmt{\isa{allI}: \isa{{\isacharparenleft}{\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymforall}x{\isachardot}\ {\isacharquery}P\ x}%
-}
-\isanewline
-\ \ \isamarkupfalse%
-\isacommand{fix}\ a\isanewline
-\ \ \isamarkupfalse%
-\isacommand{from}\ P\ \isamarkupfalse%
-\isacommand{show}\ {\isachardoublequote}P{\isacharparenleft}f\ a{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{{\isachardot}{\isachardot}}\ \ %
-\isamarkupcmt{\isa{allE}: \isa{{\isasymlbrakk}{\isasymforall}x{\isachardot}\ {\isacharquery}P\ x{\isacharsemicolon}\ {\isacharquery}P\ {\isacharquery}x\ {\isasymLongrightarrow}\ {\isacharquery}R{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}R}%
-}
-\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent Note that in the proof we have chosen to call the bound
@@ -615,29 +514,16 @@
 \isamarkuptrue%
 \isacommand{lemma}\ \isakeyword{assumes}\ Pf{\isacharcolon}\ {\isachardoublequote}{\isasymexists}x{\isachardot}\ P{\isacharparenleft}f\ x{\isacharparenright}{\isachardoublequote}\ \isakeyword{shows}\ {\isachardoublequote}{\isasymexists}y{\isachardot}\ P\ y{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{proof}\ {\isacharminus}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{from}\ Pf\ \isamarkupfalse%
-\isacommand{show}\ {\isacharquery}thesis\isanewline
-\ \ \isamarkupfalse%
-\isacommand{proof}\ \ \ \ \ \ \ \ \ \ \ \ \ \ %
-\isamarkupcmt{\isa{exE}: \isa{{\isasymlbrakk}{\isasymexists}x{\isachardot}\ {\isacharquery}P\ x{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x\ {\isasymLongrightarrow}\ {\isacharquery}Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}Q}%
-}
-\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{fix}\ x\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{assume}\ {\isachardoublequote}P{\isacharparenleft}f\ x{\isacharparenright}{\isachardoublequote}\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
-\isacommand{{\isachardot}{\isachardot}}\ \ %
-\isamarkupcmt{\isa{exI}: \isa{{\isacharquery}P\ {\isacharquery}x\ {\isasymLongrightarrow}\ {\isasymexists}x{\isachardot}\ {\isacharquery}P\ x}%
-}
-\isanewline
-\ \ \isamarkupfalse%
-\isacommand{qed}\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent Explicit $\exists$-elimination as seen above can become
@@ -648,16 +534,13 @@
 \isamarkuptrue%
 \isacommand{lemma}\ \isakeyword{assumes}\ Pf{\isacharcolon}\ {\isachardoublequote}{\isasymexists}x{\isachardot}\ P{\isacharparenleft}f\ x{\isacharparenright}{\isachardoublequote}\ \isakeyword{shows}\ {\isachardoublequote}{\isasymexists}y{\isachardot}\ P\ y{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{proof}\ {\isacharminus}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{from}\ Pf\ \isamarkupfalse%
-\isacommand{obtain}\ x\ \isakeyword{where}\ {\isachardoublequote}P{\isacharparenleft}f\ x{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{{\isachardot}{\isachardot}}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{thus}\ {\isachardoublequote}{\isasymexists}y{\isachardot}\ P\ y{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{{\isachardot}{\isachardot}}\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent Note how the proof text follows the usual mathematical style
@@ -672,21 +555,16 @@
 \isamarkuptrue%
 \isacommand{lemma}\ \isakeyword{assumes}\ ex{\isacharcolon}\ {\isachardoublequote}{\isasymexists}x{\isachardot}\ {\isasymforall}y{\isachardot}\ P\ x\ y{\isachardoublequote}\ \isakeyword{shows}\ {\isachardoublequote}{\isasymforall}y{\isachardot}\ {\isasymexists}x{\isachardot}\ P\ x\ y{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{proof}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{fix}\ y\isanewline
-\ \ \isamarkupfalse%
-\isacommand{from}\ ex\ \isamarkupfalse%
-\isacommand{obtain}\ x\ \isakeyword{where}\ {\isachardoublequote}{\isasymforall}y{\isachardot}\ P\ x\ y{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{{\isachardot}{\isachardot}}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{hence}\ {\isachardoublequote}P\ x\ y{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{{\isachardot}{\isachardot}}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{thus}\ {\isachardoublequote}{\isasymexists}x{\isachardot}\ P\ x\ y{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{{\isachardot}{\isachardot}}\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 %
 \isamarkupsubsection{Making bigger steps%
 }
@@ -701,43 +579,28 @@
 \isamarkuptrue%
 \isacommand{theorem}\ {\isachardoublequote}{\isasymexists}S{\isachardot}\ S\ {\isasymnotin}\ range\ {\isacharparenleft}f\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isacharparenright}{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{proof}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{let}\ {\isacharquery}S\ {\isacharequal}\ {\isachardoublequote}{\isacharbraceleft}x{\isachardot}\ x\ {\isasymnotin}\ f\ x{\isacharbraceright}{\isachardoublequote}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{show}\ {\isachardoublequote}{\isacharquery}S\ {\isasymnotin}\ range\ f{\isachardoublequote}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{proof}\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{assume}\ {\isachardoublequote}{\isacharquery}S\ {\isasymin}\ range\ f{\isachardoublequote}\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{then}\ \isamarkupfalse%
-\isacommand{obtain}\ y\ \isakeyword{where}\ fy{\isacharcolon}\ {\isachardoublequote}{\isacharquery}S\ {\isacharequal}\ f\ y{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{{\isachardot}{\isachardot}}\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{show}\ False\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{proof}\ cases\isanewline
-\ \ \ \ \ \ \isamarkupfalse%
-\isacommand{assume}\ {\isachardoublequote}y\ {\isasymin}\ {\isacharquery}S{\isachardoublequote}\isanewline
-\ \ \ \ \ \ \isamarkupfalse%
-\isacommand{with}\ fy\ \isamarkupfalse%
-\isacommand{show}\ False\ \isamarkupfalse%
-\isacommand{by}\ blast\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{next}\isanewline
-\ \ \ \ \ \ \isamarkupfalse%
-\isacommand{assume}\ {\isachardoublequote}y\ {\isasymnotin}\ {\isacharquery}S{\isachardoublequote}\isanewline
-\ \ \ \ \ \ \isamarkupfalse%
-\isacommand{with}\ fy\ \isamarkupfalse%
-\isacommand{show}\ False\ \isamarkupfalse%
-\isacommand{by}\ blast\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{qed}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{qed}\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent
@@ -761,53 +624,34 @@
 \isamarkuptrue%
 \isacommand{theorem}\ {\isachardoublequote}{\isasymexists}S{\isachardot}\ S\ {\isasymnotin}\ range\ {\isacharparenleft}f\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isacharparenright}{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{proof}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{let}\ {\isacharquery}S\ {\isacharequal}\ {\isachardoublequote}{\isacharbraceleft}x{\isachardot}\ x\ {\isasymnotin}\ f\ x{\isacharbraceright}{\isachardoublequote}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{show}\ {\isachardoublequote}{\isacharquery}S\ {\isasymnotin}\ range\ f{\isachardoublequote}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{proof}\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{assume}\ {\isachardoublequote}{\isacharquery}S\ {\isasymin}\ range\ f{\isachardoublequote}\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{then}\ \isamarkupfalse%
-\isacommand{obtain}\ y\ \isakeyword{where}\ fy{\isacharcolon}\ {\isachardoublequote}{\isacharquery}S\ {\isacharequal}\ f\ y{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{{\isachardot}{\isachardot}}\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{show}\ False\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{proof}\ cases\isanewline
-\ \ \ \ \ \ \isamarkupfalse%
-\isacommand{assume}\ {\isachardoublequote}y\ {\isasymin}\ {\isacharquery}S{\isachardoublequote}\isanewline
-\ \ \ \ \ \ \isamarkupfalse%
-\isacommand{hence}\ {\isachardoublequote}y\ {\isasymnotin}\ f\ y{\isachardoublequote}\ \ \ \isamarkupfalse%
-\isacommand{by}\ simp\isanewline
-\ \ \ \ \ \ \isamarkupfalse%
-\isacommand{hence}\ {\isachardoublequote}y\ {\isasymnotin}\ {\isacharquery}S{\isachardoublequote}\ \ \ \ \isamarkupfalse%
-\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}fy{\isacharparenright}\isanewline
-\ \ \ \ \ \ \isamarkupfalse%
-\isacommand{thus}\ False\ \ \ \ \ \ \ \ \ \isamarkupfalse%
-\isacommand{by}\ contradiction\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{next}\isanewline
-\ \ \ \ \ \ \isamarkupfalse%
-\isacommand{assume}\ {\isachardoublequote}y\ {\isasymnotin}\ {\isacharquery}S{\isachardoublequote}\isanewline
-\ \ \ \ \ \ \isamarkupfalse%
-\isacommand{hence}\ {\isachardoublequote}y\ {\isasymin}\ f\ y{\isachardoublequote}\ \ \ \isamarkupfalse%
-\isacommand{by}\ simp\isanewline
-\ \ \ \ \ \ \isamarkupfalse%
-\isacommand{hence}\ {\isachardoublequote}y\ {\isasymin}\ {\isacharquery}S{\isachardoublequote}\ \ \ \ \isamarkupfalse%
-\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}fy{\isacharparenright}\isanewline
-\ \ \ \ \ \ \isamarkupfalse%
-\isacommand{thus}\ False\ \ \ \ \ \ \ \ \ \isamarkupfalse%
-\isacommand{by}\ contradiction\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{qed}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{qed}\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent Method \isa{contradiction} succeeds if both $P$ and
@@ -820,7 +664,7 @@
 \isamarkuptrue%
 \isacommand{theorem}\ {\isachardoublequote}{\isasymexists}S{\isachardot}\ S\ {\isasymnotin}\ range\ {\isacharparenleft}f\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isacharparenright}{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{by}\ best\isamarkupfalse%
+\isamarkupfalse%
 %
 \isamarkupsubsection{Raw proof blocks%
 }
@@ -836,28 +680,19 @@
 \isamarkupfalse%
 \isacommand{lemma}\ {\isachardoublequote}{\isasymforall}x\ y{\isachardot}\ A\ x\ y\ {\isasymand}\ B\ x\ y\ {\isasymlongrightarrow}\ C\ x\ y{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{proof}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{fix}\ x\ \isamarkupfalse%
-\isacommand{show}\ {\isachardoublequote}{\isasymforall}y{\isachardot}\ A\ x\ y\ {\isasymand}\ B\ x\ y\ {\isasymlongrightarrow}\ C\ x\ y{\isachardoublequote}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{proof}\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{fix}\ y\ \isamarkupfalse%
-\isacommand{show}\ {\isachardoublequote}A\ x\ y\ {\isasymand}\ B\ x\ y\ {\isasymlongrightarrow}\ C\ x\ y{\isachardoublequote}\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{proof}\isanewline
-\ \ \ \ \ \ \isamarkupfalse%
-\isacommand{assume}\ {\isachardoublequote}A\ x\ y\ {\isasymand}\ B\ x\ y{\isachardoublequote}\isanewline
-\ \ \ \ \ \ \isamarkupfalse%
-\isacommand{show}\ {\isachardoublequote}C\ x\ y{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{sorry}\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{qed}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{qed}\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent Since we are only interested in the decomposition and not the
@@ -871,24 +706,17 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}{\isasymforall}x\ y{\isachardot}\ A\ x\ y\ {\isasymand}\ B\ x\ y\ {\isasymlongrightarrow}\ C\ x\ y{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{proof}\ {\isacharminus}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{have}\ {\isachardoublequote}{\isasymAnd}x\ y{\isachardot}\ {\isasymlbrakk}\ A\ x\ y{\isacharsemicolon}\ B\ x\ y\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ C\ x\ y{\isachardoublequote}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{proof}\ {\isacharminus}\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{fix}\ x\ y\ \isamarkupfalse%
-\isacommand{assume}\ {\isachardoublequote}A\ x\ y{\isachardoublequote}\ {\isachardoublequote}B\ x\ y{\isachardoublequote}\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{show}\ {\isachardoublequote}C\ x\ y{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{sorry}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{qed}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{thus}\ {\isacharquery}thesis\ \isamarkupfalse%
-\isacommand{by}\ blast\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent
@@ -898,20 +726,16 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}{\isasymforall}x\ y{\isachardot}\ A\ x\ y\ {\isasymand}\ B\ x\ y\ {\isasymlongrightarrow}\ C\ x\ y{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{proof}\ {\isacharminus}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
-\isacommand{fix}\ x\ y\ \isamarkupfalse%
-\isacommand{assume}\ {\isachardoublequote}A\ x\ y{\isachardoublequote}\ {\isachardoublequote}B\ x\ y{\isachardoublequote}\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{have}\ {\isachardoublequote}C\ x\ y{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{sorry}\ \isamarkupfalse%
-\isacommand{{\isacharbraceright}}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{thus}\ {\isacharquery}thesis\ \isamarkupfalse%
-\isacommand{by}\ blast\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent The result of the raw proof block is the same theorem
@@ -947,67 +771,31 @@
 %
 \renewcommand{\isamarkupcmt}[1]{#1}
 \isamarkupfalse%
-\isacommand{proof}\ {\isacharminus}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{have}\ {\isachardoublequote}P\isactrlisub {\isadigit{1}}\ {\isasymor}\ P\isactrlisub {\isadigit{2}}\ {\isasymor}\ P\isactrlisub {\isadigit{3}}{\isachardoublequote}\ \isamarkupfalse%
-\ %
-\isamarkupcmt{\dots%
-}
-\isanewline
-\ \ \isamarkupfalse%
-\isacommand{moreover}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
-\isacommand{assume}\ P\isactrlisub {\isadigit{1}}\isanewline
-\ \ \ \ %
-\isamarkupcmt{\dots%
-}
-\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{have}\ {\isacharquery}thesis\ \isamarkupfalse%
-\ %
-\isamarkupcmt{\dots%
-}
-\ \isamarkupfalse%
-\isacommand{{\isacharbraceright}}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{moreover}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
-\isacommand{assume}\ P\isactrlisub {\isadigit{2}}\isanewline
-\ \ \ \ %
-\isamarkupcmt{\dots%
-}
-\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{have}\ {\isacharquery}thesis\ \isamarkupfalse%
-\ %
-\isamarkupcmt{\dots%
-}
-\ \isamarkupfalse%
-\isacommand{{\isacharbraceright}}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{moreover}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
-\isacommand{assume}\ P\isactrlisub {\isadigit{3}}\isanewline
-\ \ \ \ %
-\isamarkupcmt{\dots%
-}
-\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{have}\ {\isacharquery}thesis\ \isamarkupfalse%
-\ %
-\isamarkupcmt{\dots%
-}
-\ \isamarkupfalse%
-\isacommand{{\isacharbraceright}}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{ultimately}\ \isamarkupfalse%
-\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
-\isacommand{by}\ blast\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 %
 \renewcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
 %
@@ -1090,7 +878,7 @@
 \ \ \ \ \ \ \ \ \ \ mono{\isacharcolon}\ {\isachardoublequote}{\isasymAnd}x\ y\ z{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isachardot}\ x\ {\isachargreater}\ y\ {\isasymLongrightarrow}\ x\ {\isacharplus}{\isacharplus}\ z\ {\isachargreater}\ y\ {\isacharplus}{\isacharplus}\ z{\isachardoublequote}\isanewline
 \ \ \isakeyword{shows}\ {\isachardoublequote}x\ {\isachargreater}\ y\ {\isasymLongrightarrow}\ z\ {\isacharplus}{\isacharplus}\ x\ {\isachargreater}\ z\ {\isacharplus}{\isacharplus}\ y{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ comm\ mono{\isacharparenright}\isamarkupfalse%
+\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent The concrete syntax is dropped at the end of the proof and the
@@ -1114,11 +902,10 @@
 \isamarkuptrue%
 \isacommand{lemma}\ \isakeyword{assumes}\ A{\isacharcolon}\ {\isachardoublequote}{\isasymexists}x\ y{\isachardot}\ P\ x\ y\ {\isasymand}\ Q\ x\ y{\isachardoublequote}\ \isakeyword{shows}\ {\isachardoublequote}R{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{proof}\ {\isacharminus}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{from}\ A\ \isamarkupfalse%
-\isacommand{obtain}\ x\ y\ \isakeyword{where}\ P{\isacharcolon}\ {\isachardoublequote}P\ x\ y{\isachardoublequote}\ \isakeyword{and}\ Q{\isacharcolon}\ {\isachardoublequote}Q\ x\ y{\isachardoublequote}\ \ \isamarkupfalse%
-\isacommand{by}\ blast\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 \isamarkupfalse%
 %
 \begin{isamarkuptext}%
@@ -1139,23 +926,15 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ {\isacharparenleft}A\ {\isasymlongrightarrow}\ B{\isacharparenright}\ {\isasymlongrightarrow}\ B{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{proof}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{assume}\ a{\isacharcolon}\ {\isachardoublequote}A{\isachardoublequote}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{show}\ {\isachardoublequote}{\isacharparenleft}A\ {\isasymlongrightarrow}B{\isacharparenright}\ {\isasymlongrightarrow}\ B{\isachardoublequote}\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}rule\ impI{\isacharparenright}\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}erule\ impE{\isacharparenright}\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}rule\ a{\isacharparenright}\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{apply}\ assumption\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{done}\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent You may need to resort to this technique if an
diff -r f45296bb1485 -r 5f0c8a3f0226 doc-src/IsarOverview/Isar/document/isabelle.sty
--- a/doc-src/IsarOverview/Isar/document/isabelle.sty	Mon May 02 16:28:33 2005 +0200
+++ b/doc-src/IsarOverview/Isar/document/isabelle.sty	Mon May 02 18:29:29 2005 +0200
@@ -25,15 +25,12 @@
 \newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
 \newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
 \newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
+\newcommand{\isactrlbsub}{\emph\bgroup\begin{math}{}\sb\bgroup\mbox\bgroup\isastylescript}
+\newcommand{\isactrlesub}{\egroup\egroup\end{math}\egroup}
+\newcommand{\isactrlbsup}{\emph\bgroup\begin{math}{}\sp\bgroup\mbox\bgroup\isastylescript}
+\newcommand{\isactrlesup}{\egroup\egroup\end{math}\egroup}
 \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
 
-% somewhat hackish: spanning sub/super scripts (\<^bsub>..\<^esub>)
-\newcommand{\isactrlbsub}{%
-\def\isatext##1{\isastylescript##1}\begin{math}_\bgroup}
-\newcommand{\isactrlesub}{\egroup\end{math}}
-\newcommand{\isactrlbsup}{%
-\def\isatext##1{\isastylescript##1}\begin{math}^\bgroup}
-\newcommand{\isactrlesup}{\egroup\end{math}}
 
 \newdimen\isa@parindent\newdimen\isa@parskip
 
diff -r f45296bb1485 -r 5f0c8a3f0226 doc-src/IsarOverview/Isar/document/isabellesym.sty
--- a/doc-src/IsarOverview/Isar/document/isabellesym.sty	Mon May 02 16:28:33 2005 +0200
+++ b/doc-src/IsarOverview/Isar/document/isabellesym.sty	Mon May 02 18:29:29 2005 +0200
@@ -6,16 +6,16 @@
 
 % symbol definitions
 
-\newcommand{\isasymzero}{\isamath{\mathbf{0}}}  %requires amssym
-\newcommand{\isasymone}{\isamath{\mathbf{1}}}   %requires amssym
-\newcommand{\isasymtwo}{\isamath{\mathbf{2}}}   %requires amssym
-\newcommand{\isasymthree}{\isamath{\mathbf{3}}} %requires amssym
-\newcommand{\isasymfour}{\isamath{\mathbf{4}}}  %requires amssym
-\newcommand{\isasymfive}{\isamath{\mathbf{5}}}  %requires amssym
-\newcommand{\isasymsix}{\isamath{\mathbf{6}}}   %requires amssym
-\newcommand{\isasymseven}{\isamath{\mathbf{7}}} %requires amssym
-\newcommand{\isasymeight}{\isamath{\mathbf{8}}} %requires amssym
-\newcommand{\isasymnine}{\isamath{\mathbf{9}}}  %requires amssym
+\newcommand{\isasymzero}{\isamath{\mathbf{0}}}  %requires amssymb
+\newcommand{\isasymone}{\isamath{\mathbf{1}}}   %requires amssymb
+\newcommand{\isasymtwo}{\isamath{\mathbf{2}}}   %requires amssymb
+\newcommand{\isasymthree}{\isamath{\mathbf{3}}} %requires amssymb
+\newcommand{\isasymfour}{\isamath{\mathbf{4}}}  %requires amssymb
+\newcommand{\isasymfive}{\isamath{\mathbf{5}}}  %requires amssymb
+\newcommand{\isasymsix}{\isamath{\mathbf{6}}}   %requires amssymb
+\newcommand{\isasymseven}{\isamath{\mathbf{7}}} %requires amssymb
+\newcommand{\isasymeight}{\isamath{\mathbf{8}}} %requires amssymb
+\newcommand{\isasymnine}{\isamath{\mathbf{9}}}  %requires amssymb
 \newcommand{\isasymA}{\isamath{\mathcal{A}}}
 \newcommand{\isasymB}{\isamath{\mathcal{B}}}
 \newcommand{\isasymC}{\isamath{\mathcal{C}}}
@@ -183,7 +183,12 @@
 \newcommand{\isasymleftharpoonup}{\isamath{\leftharpoonup}}
 \newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}}
 \newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}}
-\newcommand{\isasymleadsto}{\isamath{\leadsto}}  %requires amssym
+\newcommand{\isasymdownharpoonleft}{\isamath{\downharpoonleft}}  %requires amssymb
+\newcommand{\isasymdownharpoonright}{\isamath{\downharpoonright}}  %requires amssymb
+\newcommand{\isasymupharpoonleft}{\isamath{\upharpoonleft}}  %requires amssymb
+\newcommand{\isasymupharpoonright}{\isamath{\upharpoonright}}  %requires amssymb
+\newcommand{\isasymrestriction}{\isamath{\restriction}}  %requires amssymb
+\newcommand{\isasymleadsto}{\isamath{\leadsto}}  %requires amssymb
 \newcommand{\isasymup}{\isamath{\uparrow}}
 \newcommand{\isasymUp}{\isamath{\Uparrow}}
 \newcommand{\isasymdown}{\isamath{\downarrow}}
@@ -214,8 +219,8 @@
 \newcommand{\isasymOr}{\isamath{\bigvee}}
 \newcommand{\isasymforall}{\isamath{\forall\,}}
 \newcommand{\isasymexists}{\isamath{\exists\,}}
-\newcommand{\isasymbox}{\isamath{\Box}}  %requires amssym
-\newcommand{\isasymdiamond}{\isamath{\Diamond}}  %requires amssym
+\newcommand{\isasymbox}{\isamath{\Box}}  %requires amssymb
+\newcommand{\isasymdiamond}{\isamath{\Diamond}}  %requires amssymb
 \newcommand{\isasymturnstile}{\isamath{\vdash}}
 \newcommand{\isasymTurnstile}{\isamath{\models}}
 \newcommand{\isasymtturnstile}{\isamath{\vdash\!\!\!\vdash}}
@@ -236,8 +241,8 @@
 \newcommand{\isasymsupset}{\isamath{\supset}}
 \newcommand{\isasymsubseteq}{\isamath{\subseteq}}
 \newcommand{\isasymsupseteq}{\isamath{\supseteq}}
-\newcommand{\isasymsqsubset}{\isamath{\sqsubset}}
-\newcommand{\isasymsqsupset}{\isamath{\sqsupset}}  %requires amssym
+\newcommand{\isasymsqsubset}{\isamath{\sqsubset}}  %requires amssymb
+\newcommand{\isasymsqsupset}{\isamath{\sqsupset}}  %requires amssymb
 \newcommand{\isasymsqsubseteq}{\isamath{\sqsubseteq}}
 \newcommand{\isasymsqsupseteq}{\isamath{\sqsupseteq}}
 \newcommand{\isasyminter}{\isamath{\cap}}
@@ -247,7 +252,7 @@
 \newcommand{\isasymsqunion}{\isamath{\sqcup}}
 \newcommand{\isasymSqunion}{\isamath{\bigsqcup\,}}
 \newcommand{\isasymsqinter}{\isamath{\sqcap}}
-\newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}}  %requires masmath
+\newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}}  %requires amsmath
 \newcommand{\isasymuplus}{\isamath{\uplus}}
 \newcommand{\isasymUplus}{\isamath{\biguplus\,}}
 \newcommand{\isasymnoteq}{\isamath{\not=}}
@@ -261,6 +266,8 @@
 \newcommand{\isasymequiv}{\isamath{\equiv}}
 \newcommand{\isasymfrown}{\isamath{\frown}}
 \newcommand{\isasympropto}{\isamath{\propto}}
+\newcommand{\isasymsome}{\isamath{\epsilon\,}}
+\newcommand{\isasymJoin}{\isamath{\Join}}  %requires amssymb
 \newcommand{\isasymbowtie}{\isamath{\bowtie}}
 \newcommand{\isasymprec}{\isamath{\prec}}
 \newcommand{\isasymsucc}{\isamath{\succ}}
@@ -278,10 +285,10 @@
 \newcommand{\isasymcirc}{\isamath{\circ}}
 \newcommand{\isasymdagger}{\isamath{\dagger}}
 \newcommand{\isasymddagger}{\isamath{\ddagger}}
-\newcommand{\isasymlhd}{\isamath{\lhd}}
-\newcommand{\isasymrhd}{\isamath{\rhd}}
-\newcommand{\isasymunlhd}{\isamath{\unlhd}}
-\newcommand{\isasymunrhd}{\isamath{\unrhd}}
+\newcommand{\isasymlhd}{\isamath{\lhd}}  %requires amssymb
+\newcommand{\isasymrhd}{\isamath{\rhd}}  %requires amssymb
+\newcommand{\isasymunlhd}{\isamath{\unlhd}}  %requires amssymb
+\newcommand{\isasymunrhd}{\isamath{\unrhd}}  %requires amssymb
 \newcommand{\isasymtriangleleft}{\isamath{\triangleleft}}
 \newcommand{\isasymtriangleright}{\isamath{\triangleright}}
 \newcommand{\isasymtriangle}{\isamath{\triangle}}
@@ -339,9 +346,8 @@
 \newcommand{\isasymcurrency}{\isatext{\textcurrency}} %requires textcomp
 \newcommand{\isasymdegree}{\isatext{\rm\textdegree}}  %requires latin1
 \newcommand{\isasymamalg}{\isamath{\amalg}}
-\newcommand{\isasymmho}{\isamath{\mho}}  %requires amssym
-\newcommand{\isasymlozenge}{\isamath{\lozenge}}  %requires amssym
-\newcommand{\isasymJoin}{\isamath{\Join}}  %requires amssym
+\newcommand{\isasymmho}{\isamath{\mho}}  %requires amssymb
+\newcommand{\isasymlozenge}{\isamath{\lozenge}}  %requires amssymb
 \newcommand{\isasymwp}{\isamath{\wp}}
 \newcommand{\isasymwrong}{\isamath{\wr}}
 \newcommand{\isasymstruct}{\isamath{\diamond}}