# HG changeset patch
# User wenzelm
# Date 1023272654 -7200
# Node ID 53022e5f73ff72dd3b2e77605510483131ab143f
# Parent  3cc108872aca78edf8c54c14f8a2780acf1637ac
initial setup;

diff -r 3cc108872aca -r 53022e5f73ff doc-src/IsarTut/IsaMakefile
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarTut/IsaMakefile	Wed Jun 05 12:24:14 2002 +0200
@@ -0,0 +1,34 @@
+
+## targets
+
+default: Tutorial
+images:
+test: Tutorial
+
+all: images test
+
+
+## global settings
+
+SRC = $(ISABELLE_HOME)/src
+OUT = $(ISABELLE_OUTPUT)
+LOG = $(OUT)/log
+USEDIR = $(ISATOOL) usedir -i true -d "" -D ../generated
+
+
+## Tutorial
+
+Tutorial: HOL $(LOG)/HOL-Tutorial.gz
+
+HOL:
+	@cd $(SRC)/HOL; $(ISATOOL) make HOL
+
+$(LOG)/HOL-Tutorial.gz: $(OUT)/HOL Tutorial/ROOT.ML Tutorial/Tutorial.thy
+	@$(USEDIR) $(OUT)/HOL Tutorial
+	@rm -f generated/pdfsetup.sty generated/session.tex
+
+
+## clean
+
+clean:
+	@rm -f $(LOG)/HOL-Tutorial.gz
diff -r 3cc108872aca -r 53022e5f73ff doc-src/IsarTut/Makefile
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarTut/Makefile	Wed Jun 05 12:24:14 2002 +0200
@@ -0,0 +1,38 @@
+#
+# $Id$
+#
+
+## targets
+
+default: dvi
+
+
+## dependencies
+
+include ../Makefile.in
+
+NAME = isar-tutorial
+
+FILES = isar-tutorial.tex ../isar.sty ../iman.sty ../extra.sty ../manual.bib \
+  generated/Tutorial.tex
+
+dvi: $(NAME).dvi
+
+$(NAME).dvi: $(FILES) isabelle_isar.eps
+	$(LATEX) $(NAME)
+	$(BIBTEX) $(NAME)
+	$(LATEX) $(NAME)
+	$(LATEX) $(NAME)
+	$(SEDINDEX) $(NAME)
+	$(LATEX) $(NAME)
+
+pdf: $(NAME).pdf
+
+$(NAME).pdf: $(FILES) isabelle_isar.pdf
+	$(PDFLATEX) $(NAME)
+	$(BIBTEX) $(NAME)
+	$(PDFLATEX) $(NAME)
+	$(PDFLATEX) $(NAME)
+	$(SEDINDEX) $(NAME)
+	$(FIXBOOKMARKS) $(NAME).out
+	$(PDFLATEX) $(NAME)
diff -r 3cc108872aca -r 53022e5f73ff doc-src/IsarTut/Tutorial/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarTut/Tutorial/ROOT.ML	Wed Jun 05 12:24:14 2002 +0200
@@ -0,0 +1,4 @@
+
+set quick_and_dirty;
+
+use_thy "Tutorial";
diff -r 3cc108872aca -r 53022e5f73ff doc-src/IsarTut/Tutorial/Tutorial.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarTut/Tutorial/Tutorial.thy	Wed Jun 05 12:24:14 2002 +0200
@@ -0,0 +1,307 @@
+
+(*<*)
+theory Tutorial = Main:
+(*>*)
+
+chapter {* Introduction *}
+
+chapter {* Interaction and debugging *}
+
+chapter {* Calculational reasoning *}
+
+chapter {* Proof by cases and induction *}
+
+chapter {* General natural deduction *}
+
+chapter {* Example: FIXME *}
+
+
+chapter FIXME
+
+
+section {* Formal document preparation *}
+
+subsection {* Example *}
+
+text {*
+  See this very document itself.
+*}
+
+subsection {* Getting started *}
+
+text {*
+  \verb"isatool mkdir Test && isatool make"
+*}
+
+section {* Human-readable proof composition in Isar *}
+
+subsection {* Getting started *}
+
+text {* Claim a trivial goal in order to enter proof mode @{text \<dots>} *}
+
+lemma True
+proof
+
+  txt {* After the canonical initial refinement step we are left
+    within an \emph{proof body}. *}
+
+  txt {* Here we may augment the present local {proof context} as we
+    please. *}
+
+  fix something
+  assume a: "anything something"
+
+  txt {* Note that the present configuration may be inspected by
+  several \emph{diagnostic commands}. *}
+
+  term something  -- "@{term [show_types] something}"
+  term anything  -- "@{term [show_types] anything}"
+  thm a  -- {* @{thm a} *}
+
+  txt {* We may state local (auxiliary) results as well. *}
+
+  have True proof qed
+
+  txt {* We are now satisfied. *}
+qed
+
+
+subsection {* Calculational Reasoning *}
+
+text {*
+  Isar is mainly about Natural Deduction, but Calculational Reasoning
+  turns out as a simplified instance of that, so we demonstrate it
+  first.
+*}
+
+subsubsection {* Transitive chains *}
+
+text {*
+  Technique: establish a chain of local facts, separated by \cmd{also}
+  and terminated by \cmd{finally}; another goal has to follow to point
+  out the final result.
+*}
+
+lemma "x1 = x4"
+proof -  -- "do nothing yet"
+  have "x1 = x2" sorry
+  also
+  have "x2 = x3" sorry
+  also
+  have "x3 = x4" sorry
+  finally
+  show "x1 = x4" .
+qed
+
+text {*
+  This may be written more succinctly, using the special term binds
+  ``@{text \<dots>}'' (for the right-hand side of the last statement) and
+  ``@{text ?thesis}'' (for the original claim at the head of the
+  proof).
+*}
+
+lemma "x1 = x4"
+proof -
+  have "x1 = x2" sorry
+  also have "\<dots> = x3" sorry
+  also have "\<dots> = x4" sorry
+  finally show ?thesis .
+qed
+
+text {*
+  The (implicit) forward-chaining steps involved in \cmd{also} and
+  \cmd{finally} are declared in the current context.  The main library
+  of Isabelle/HOL already knows about (mixed) transitivities of @{text
+  "="}, @{text "<"}, @{text "\<le>"} etc.
+*}
+
+lemma "(x1::nat) < x6"
+  -- {* restriction to type @{typ nat} ensures that @{text "<"} is really transitive *}
+proof -
+  have "x1 < x2" sorry
+  also have "\<dots> \<le> x3" sorry
+  also have "\<dots> = x4" sorry
+  also have "\<dots> < x5" sorry
+  also have "\<dots> = x6" sorry
+  finally show ?thesis .
+qed
+
+text {*
+  We may also calculate on propositions.
+*}
+
+lemma True
+proof
+  have "A \<longrightarrow> B \<longrightarrow> C" sorry
+  also have A sorry
+  also have B sorry
+  finally have C .
+qed    
+
+text {*
+  This is getting pretty close to Dijkstra's preferred proof style.
+*}
+
+lemma True
+proof
+  have [trans]: "\<And>X Y Z. X \<longrightarrow> Y \<Longrightarrow> Y \<longrightarrow> Z \<Longrightarrow> X \<longrightarrow> Z" by rules
+  have "A \<longrightarrow> B" sorry
+  also have "\<dots> \<longrightarrow> C" sorry
+  also have "\<dots> \<longrightarrow> D" sorry
+  finally have "A \<longrightarrow> D" .
+qed
+
+
+subsubsection {* Degenerate calculations and bigstep reasoning *}
+
+text {*
+  Instead of \cmd{also}/\cmd{finally} we may use degenerative steps
+  \cmd{moreover}/\cmd{ultimately} to accumulate facts, without
+  applying any forward rules yet.
+*}
+
+lemma True
+proof
+  have A sorry
+  moreover have B sorry
+  moreover have C sorry
+  ultimately have A and B and C .  -- "Pretty obvious, right?"
+qed
+
+text {*
+  Both kinds of calculational elements may be used together.
+*}
+
+lemma True
+proof
+  assume reasoning_pattern [trans]: "A \<Longrightarrow> B \<Longrightarrow> C \<Longrightarrow> D"
+  have A sorry
+  moreover have B sorry
+  moreover have C sorry
+  finally have D .
+qed
+  
+
+subsection {* Natural deduction *}
+
+subsubsection {* Primitive patterns *}
+
+text {*
+  The default theory context admits to perform canonical single-step
+  reasoning (similar to Gentzen) without further ado.
+*}
+
+lemma True
+proof
+
+  have True ..
+
+  { assume False
+    then have C .. }
+
+  have "\<not> A"
+  proof
+    assume A
+    show False sorry
+  qed
+
+  { assume "\<not> A" and A
+    then have C .. }
+
+  have "A \<longrightarrow> B"
+  proof
+    assume A
+    show B sorry
+  qed
+
+  { assume "A \<longrightarrow> B" and A
+    then have B .. }
+
+  have "A \<and> B"
+  proof
+    show A sorry
+    show B sorry
+  qed
+
+  { assume "A \<and> B"
+    then have A .. }
+
+  { assume "A \<and> B"
+    then have B .. }
+
+  { assume A
+    then have "A \<or> B" .. }
+
+  { assume B
+    then have "A \<or> B" .. }
+
+  { assume "A \<or> B"
+    then have C
+    proof
+      assume A
+      then show ?thesis sorry
+    next
+      assume B
+      then show ?thesis sorry
+    qed }
+
+  have "\<forall>x. P x"
+  proof
+    fix x
+    show "P x" sorry
+  qed
+
+  { assume "\<forall>x. P x"
+    then have "P t" .. }
+
+  have "\<exists>x. P x"
+  proof
+    show "P t" sorry
+  qed
+  
+  { assume "\<exists>x. P x"
+    then obtain x where "P x" ..
+    note nothing  -- "relax" }
+qed
+
+text {*
+  Certainly, this works with derived rules for defined concepts in the
+  same manner.  E.g.\ use the simple-typed set-theory of Isabelle/HOL. *}
+
+lemma True
+proof
+  have "y \<in> (\<Inter>x \<in> A. B x)"
+  proof
+    fix x
+    assume "x \<in> A"
+    show "y \<in> B x" sorry
+  qed
+
+  have "y \<in> (\<Union>x \<in> A. B x)"
+  proof
+    show "a \<in> A" sorry
+    show "y \<in> B a" sorry
+  qed
+qed
+
+
+subsubsection {* Variations in structure *}
+
+text {*
+  The design of the Isar language takes the user seriously
+*}
+
+subsubsection {* Generalized elimination *}
+
+subsubsection {* Scalable cases and induction *}
+
+section {* Assimilating the old tactical style *}
+
+text {*
+  Improper commands: 
+  Observation: every Isar subproof may start with a ``script'' of
+*}
+
+(*<*)
+end
+(*>*)
diff -r 3cc108872aca -r 53022e5f73ff doc-src/IsarTut/generated/Tutorial.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarTut/generated/Tutorial.tex	Wed Jun 05 12:24:14 2002 +0200
@@ -0,0 +1,612 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Tutorial}%
+\isamarkupfalse%
+%
+\isamarkupchapter{Introduction%
+}
+\isamarkuptrue%
+%
+\isamarkupchapter{Interaction and debugging%
+}
+\isamarkuptrue%
+%
+\isamarkupchapter{Calculational reasoning%
+}
+\isamarkuptrue%
+%
+\isamarkupchapter{Proof by cases and induction%
+}
+\isamarkuptrue%
+%
+\isamarkupchapter{General natural deduction%
+}
+\isamarkuptrue%
+%
+\isamarkupchapter{Example: FIXME%
+}
+\isamarkuptrue%
+%
+\isamarkupchapter{FIXME%
+}
+\isamarkuptrue%
+%
+\isamarkupsection{Formal document preparation%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsection{Example%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+See this very document itself.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Getting started%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\verb"isatool mkdir Test && isatool make"%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Human-readable proof composition in Isar%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsection{Getting started%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Claim a trivial goal in order to enter proof mode \isa{{\isasymdots}}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ True\isanewline
+\isamarkupfalse%
+\isacommand{proof}\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+After the canonical initial refinement step we are left
+    within an \emph{proof body}.%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+%
+\begin{isamarkuptxt}%
+Here we may augment the present local {proof context} as we
+    please.%
+\end{isamarkuptxt}%
+\ \ \isamarkuptrue%
+\isacommand{fix}\ something\isanewline
+\ \ \isamarkupfalse%
+\isacommand{assume}\ a{\isacharcolon}\ {\isachardoublequote}anything\ something{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+Note that the present configuration may be inspected by
+  several \emph{diagnostic commands}.%
+\end{isamarkuptxt}%
+\ \ \isamarkuptrue%
+\isacommand{term}\ something\ \ %
+\isamarkupcmt{\isa{something{\isasymColon}{\isacharprime}a}%
+}
+\isanewline
+\ \ \isamarkupfalse%
+\isacommand{term}\ anything\ \ %
+\isamarkupcmt{\isa{anything{\isasymColon}{\isacharprime}a\ {\isasymRightarrow}\ bool}%
+}
+\isanewline
+\ \ \isamarkupfalse%
+\isacommand{thm}\ a\ \ %
+\isamarkupcmt{\isa{anything\ something}%
+}
+\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+We may state local (auxiliary) results as well.%
+\end{isamarkuptxt}%
+\ \ \isamarkuptrue%
+\isacommand{have}\ True\ \isamarkupfalse%
+\isacommand{proof}\ \isamarkupfalse%
+\isacommand{qed}\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+We are now satisfied.%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\isacommand{qed}\isamarkupfalse%
+%
+\isamarkupsubsection{Calculational Reasoning%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Isar is mainly about Natural Deduction, but Calculational Reasoning
+  turns out as a simplified instance of that, so we demonstrate it
+  first.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Transitive chains%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Technique: establish a chain of local facts, separated by \cmd{also}
+  and terminated by \cmd{finally}; another goal has to follow to point
+  out the final result.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ {\isachardoublequote}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{4}}{\isachardoublequote}\isanewline
+\isamarkupfalse%
+\isacommand{proof}\ {\isacharminus}\ \ %
+\isamarkupcmt{do nothing yet%
+}
+\isanewline
+\ \ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{also}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}x{\isadigit{2}}\ {\isacharequal}\ x{\isadigit{3}}{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{also}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}x{\isadigit{3}}\ {\isacharequal}\ x{\isadigit{4}}{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{finally}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{show}\ {\isachardoublequote}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{4}}{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{{\isachardot}}\isanewline
+\isamarkupfalse%
+\isacommand{qed}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+This may be written more succinctly, using the special term binds
+  ``\isa{{\isasymdots}}'' (for the right-hand side of the last statement) and
+  ``\isa{{\isacharquery}thesis}'' (for the original claim at the head of the
+  proof).%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ {\isachardoublequote}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{4}}{\isachardoublequote}\isanewline
+\isamarkupfalse%
+\isacommand{proof}\ {\isacharminus}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{also}\ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isacharequal}\ x{\isadigit{3}}{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{also}\ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isacharequal}\ x{\isadigit{4}}{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{finally}\ \isamarkupfalse%
+\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
+\isacommand{{\isachardot}}\isanewline
+\isamarkupfalse%
+\isacommand{qed}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+The (implicit) forward-chaining steps involved in \cmd{also} and
+  \cmd{finally} are declared in the current context.  The main library
+  of Isabelle/HOL already knows about (mixed) transitivities of \isa{{\isacharequal}}, \isa{{\isacharless}}, \isa{{\isasymle}} etc.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}x{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ {\isacharless}\ x{\isadigit{6}}{\isachardoublequote}\isanewline
+\ \ %
+\isamarkupcmt{restriction to type \isa{nat} ensures that \isa{{\isacharless}} is really transitive%
+}
+\isanewline
+\isamarkupfalse%
+\isacommand{proof}\ {\isacharminus}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{also}\ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isasymle}\ x{\isadigit{3}}{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{also}\ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isacharequal}\ x{\isadigit{4}}{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{also}\ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isacharless}\ x{\isadigit{5}}{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{also}\ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isacharequal}\ x{\isadigit{6}}{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{finally}\ \isamarkupfalse%
+\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
+\isacommand{{\isachardot}}\isanewline
+\isamarkupfalse%
+\isacommand{qed}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+We may also calculate on propositions.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ True\isanewline
+\isamarkupfalse%
+\isacommand{proof}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ B\ {\isasymlongrightarrow}\ C{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{also}\ \isamarkupfalse%
+\isacommand{have}\ A\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{also}\ \isamarkupfalse%
+\isacommand{have}\ B\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{finally}\ \isamarkupfalse%
+\isacommand{have}\ C\ \isamarkupfalse%
+\isacommand{{\isachardot}}\isanewline
+\isamarkupfalse%
+\isacommand{qed}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+This is getting pretty close to Dijkstra's preferred proof style.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ True\isanewline
+\isamarkupfalse%
+\isacommand{proof}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{have}\ {\isacharbrackleft}trans{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymAnd}X\ Y\ Z{\isachardot}\ X\ {\isasymlongrightarrow}\ Y\ {\isasymLongrightarrow}\ Y\ {\isasymlongrightarrow}\ Z\ {\isasymLongrightarrow}\ X\ {\isasymlongrightarrow}\ Z{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{by}\ rules\isanewline
+\ \ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ B{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{also}\ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isasymlongrightarrow}\ C{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{also}\ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isasymlongrightarrow}\ D{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{finally}\ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ D{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{{\isachardot}}\isanewline
+\isamarkupfalse%
+\isacommand{qed}\isamarkupfalse%
+%
+\isamarkupsubsubsection{Degenerate calculations and bigstep reasoning%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Instead of \cmd{also}/\cmd{finally} we may use degenerative steps
+  \cmd{moreover}/\cmd{ultimately} to accumulate facts, without
+  applying any forward rules yet.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ True\isanewline
+\isamarkupfalse%
+\isacommand{proof}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{have}\ A\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{moreover}\ \isamarkupfalse%
+\isacommand{have}\ B\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{moreover}\ \isamarkupfalse%
+\isacommand{have}\ C\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{ultimately}\ \isamarkupfalse%
+\isacommand{have}\ A\ \isakeyword{and}\ B\ \isakeyword{and}\ C\ \isamarkupfalse%
+\isacommand{{\isachardot}}\ \ %
+\isamarkupcmt{Pretty obvious, right?%
+}
+\isanewline
+\isamarkupfalse%
+\isacommand{qed}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Both kinds of calculational elements may be used together.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ True\isanewline
+\isamarkupfalse%
+\isacommand{proof}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{assume}\ reasoning{\isacharunderscore}pattern\ {\isacharbrackleft}trans{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}A\ {\isasymLongrightarrow}\ B\ {\isasymLongrightarrow}\ C\ {\isasymLongrightarrow}\ D{\isachardoublequote}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{have}\ A\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{moreover}\ \isamarkupfalse%
+\isacommand{have}\ B\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{moreover}\ \isamarkupfalse%
+\isacommand{have}\ C\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{finally}\ \isamarkupfalse%
+\isacommand{have}\ D\ \isamarkupfalse%
+\isacommand{{\isachardot}}\isanewline
+\isamarkupfalse%
+\isacommand{qed}\isamarkupfalse%
+%
+\isamarkupsubsection{Natural deduction%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Primitive patterns%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The default theory context admits to perform canonical single-step
+  reasoning (similar to Gentzen) without further ado.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ True\isanewline
+\isamarkupfalse%
+\isacommand{proof}\isanewline
+\isanewline
+\ \ \isamarkupfalse%
+\isacommand{have}\ True\ \isamarkupfalse%
+\isacommand{{\isachardot}{\isachardot}}\isanewline
+\isanewline
+\ \ \isamarkupfalse%
+\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
+\isacommand{assume}\ False\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{then}\ \isamarkupfalse%
+\isacommand{have}\ C\ \isamarkupfalse%
+\isacommand{{\isachardot}{\isachardot}}\ \isamarkupfalse%
+\isacommand{{\isacharbraceright}}\isanewline
+\isanewline
+\ \ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}{\isasymnot}\ A{\isachardoublequote}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{proof}\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{assume}\ A\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{show}\ False\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{qed}\isanewline
+\isanewline
+\ \ \isamarkupfalse%
+\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
+\isacommand{assume}\ {\isachardoublequote}{\isasymnot}\ A{\isachardoublequote}\ \isakeyword{and}\ A\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{then}\ \isamarkupfalse%
+\isacommand{have}\ C\ \isamarkupfalse%
+\isacommand{{\isachardot}{\isachardot}}\ \isamarkupfalse%
+\isacommand{{\isacharbraceright}}\isanewline
+\isanewline
+\ \ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ B{\isachardoublequote}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{proof}\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{assume}\ A\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{show}\ B\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{qed}\isanewline
+\isanewline
+\ \ \isamarkupfalse%
+\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
+\isacommand{assume}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ B{\isachardoublequote}\ \isakeyword{and}\ A\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{then}\ \isamarkupfalse%
+\isacommand{have}\ B\ \isamarkupfalse%
+\isacommand{{\isachardot}{\isachardot}}\ \isamarkupfalse%
+\isacommand{{\isacharbraceright}}\isanewline
+\isanewline
+\ \ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{proof}\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{show}\ A\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{show}\ B\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{qed}\isanewline
+\isanewline
+\ \ \isamarkupfalse%
+\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
+\isacommand{assume}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{then}\ \isamarkupfalse%
+\isacommand{have}\ A\ \isamarkupfalse%
+\isacommand{{\isachardot}{\isachardot}}\ \isamarkupfalse%
+\isacommand{{\isacharbraceright}}\isanewline
+\isanewline
+\ \ \isamarkupfalse%
+\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
+\isacommand{assume}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{then}\ \isamarkupfalse%
+\isacommand{have}\ B\ \isamarkupfalse%
+\isacommand{{\isachardot}{\isachardot}}\ \isamarkupfalse%
+\isacommand{{\isacharbraceright}}\isanewline
+\isanewline
+\ \ \isamarkupfalse%
+\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
+\isacommand{assume}\ A\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{then}\ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}A\ {\isasymor}\ B{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{{\isachardot}{\isachardot}}\ \isamarkupfalse%
+\isacommand{{\isacharbraceright}}\isanewline
+\isanewline
+\ \ \isamarkupfalse%
+\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
+\isacommand{assume}\ B\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{then}\ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}A\ {\isasymor}\ B{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{{\isachardot}{\isachardot}}\ \isamarkupfalse%
+\isacommand{{\isacharbraceright}}\isanewline
+\isanewline
+\ \ \isamarkupfalse%
+\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
+\isacommand{assume}\ {\isachardoublequote}A\ {\isasymor}\ B{\isachardoublequote}\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{then}\ \isamarkupfalse%
+\isacommand{have}\ C\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{proof}\isanewline
+\ \ \ \ \ \ \isamarkupfalse%
+\isacommand{assume}\ A\isanewline
+\ \ \ \ \ \ \isamarkupfalse%
+\isacommand{then}\ \isamarkupfalse%
+\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{next}\isanewline
+\ \ \ \ \ \ \isamarkupfalse%
+\isacommand{assume}\ B\isanewline
+\ \ \ \ \ \ \isamarkupfalse%
+\isacommand{then}\ \isamarkupfalse%
+\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{qed}\ \isamarkupfalse%
+\isacommand{{\isacharbraceright}}\isanewline
+\isanewline
+\ \ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}{\isasymforall}x{\isachardot}\ P\ x{\isachardoublequote}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{proof}\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{fix}\ x\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{show}\ {\isachardoublequote}P\ x{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{qed}\isanewline
+\isanewline
+\ \ \isamarkupfalse%
+\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
+\isacommand{assume}\ {\isachardoublequote}{\isasymforall}x{\isachardot}\ P\ x{\isachardoublequote}\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{then}\ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}P\ t{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{{\isachardot}{\isachardot}}\ \isamarkupfalse%
+\isacommand{{\isacharbraceright}}\isanewline
+\isanewline
+\ \ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}{\isasymexists}x{\isachardot}\ P\ x{\isachardoublequote}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{proof}\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{show}\ {\isachardoublequote}P\ t{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{qed}\isanewline
+\ \ \isanewline
+\ \ \isamarkupfalse%
+\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
+\isacommand{assume}\ {\isachardoublequote}{\isasymexists}x{\isachardot}\ P\ x{\isachardoublequote}\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{then}\ \isamarkupfalse%
+\isacommand{obtain}\ x\ \isakeyword{where}\ {\isachardoublequote}P\ x{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{{\isachardot}{\isachardot}}\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{note}\ nothing\ \ %
+\isamarkupcmt{relax%
+}
+\ \isamarkupfalse%
+\isacommand{{\isacharbraceright}}\isanewline
+\isamarkupfalse%
+\isacommand{qed}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Certainly, this works with derived rules for defined concepts in the
+  same manner.  E.g.\ use the simple-typed set-theory of Isabelle/HOL.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ True\isanewline
+\isamarkupfalse%
+\isacommand{proof}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}y\ {\isasymin}\ {\isacharparenleft}{\isasymInter}x\ {\isasymin}\ A{\isachardot}\ B\ x{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{proof}\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{fix}\ x\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{assume}\ {\isachardoublequote}x\ {\isasymin}\ A{\isachardoublequote}\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{show}\ {\isachardoublequote}y\ {\isasymin}\ B\ x{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{qed}\isanewline
+\isanewline
+\ \ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}y\ {\isasymin}\ {\isacharparenleft}{\isasymUnion}x\ {\isasymin}\ A{\isachardot}\ B\ x{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{proof}\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{show}\ {\isachardoublequote}a\ {\isasymin}\ A{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{show}\ {\isachardoublequote}y\ {\isasymin}\ B\ a{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{qed}\isanewline
+\isamarkupfalse%
+\isacommand{qed}\isamarkupfalse%
+%
+\isamarkupsubsubsection{Variations in structure%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The design of the Isar language takes the user seriously%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Generalized elimination%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Scalable cases and induction%
+}
+\isamarkuptrue%
+%
+\isamarkupsection{Assimilating the old tactical style%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Improper commands: 
+  Observation: every Isar subproof may start with a ``script'' of%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isamarkupfalse%
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 3cc108872aca -r 53022e5f73ff doc-src/IsarTut/generated/isabelle.sty
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarTut/generated/isabelle.sty	Wed Jun 05 12:24:14 2002 +0200
@@ -0,0 +1,157 @@
+%%
+%% Author: Markus Wenzel, TU Muenchen
+%% License: GPL (GNU GENERAL PUBLIC LICENSE)
+%%
+%% macros for Isabelle generated LaTeX output
+%%
+
+%%% Simple document preparation (based on theory token language and symbols)
+
+% isabelle environments
+
+\newcommand{\isabellecontext}{UNKNOWN}
+
+\newcommand{\isastyle}{\small\tt\slshape}
+\newcommand{\isastyleminor}{\small\tt\slshape}
+\newcommand{\isastylescript}{\footnotesize\tt\slshape}
+\newcommand{\isastyletext}{\normalsize\rm}
+\newcommand{\isastyletxt}{\rm}
+\newcommand{\isastylecmt}{\rm}
+
+%symbol markup -- \emph achieves decent spacing via italic corrections
+\newcommand{\isamath}[1]{\emph{$#1$}}
+\newcommand{\isatext}[1]{\emph{#1}}
+\newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
+\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
+\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
+\newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
+
+\newdimen\isa@parindent\newdimen\isa@parskip
+
+\newenvironment{isabellebody}{%
+\isamarkuptrue\par%
+\isa@parindent\parindent\parindent0pt%
+\isa@parskip\parskip\parskip0pt%
+\isastyle}{\par}
+
+\newenvironment{isabelle}
+{\begin{trivlist}\begin{isabellebody}\item\relax}
+{\end{isabellebody}\end{trivlist}}
+
+\newcommand{\isa}[1]{\emph{\isastyleminor #1}}
+
+\newcommand{\isaindent}[1]{\hphantom{#1}}
+\newcommand{\isanewline}{\mbox{}\\\mbox{}}
+\newcommand{\isadigit}[1]{#1}
+
+\chardef\isacharbang=`\!
+\chardef\isachardoublequote=`\"
+\chardef\isacharhash=`\#
+\chardef\isachardollar=`\$
+\chardef\isacharpercent=`\%
+\chardef\isacharampersand=`\&
+\chardef\isacharprime=`\'
+\chardef\isacharparenleft=`\(
+\chardef\isacharparenright=`\)
+\chardef\isacharasterisk=`\*
+\chardef\isacharplus=`\+
+\chardef\isacharcomma=`\,
+\chardef\isacharminus=`\-
+\chardef\isachardot=`\.
+\chardef\isacharslash=`\/
+\chardef\isacharcolon=`\:
+\chardef\isacharsemicolon=`\;
+\chardef\isacharless=`\<
+\chardef\isacharequal=`\=
+\chardef\isachargreater=`\>
+\chardef\isacharquery=`\?
+\chardef\isacharat=`\@
+\chardef\isacharbrackleft=`\[
+\chardef\isacharbackslash=`\\
+\chardef\isacharbrackright=`\]
+\chardef\isacharcircum=`\^
+\chardef\isacharunderscore=`\_
+\chardef\isacharbackquote=`\`
+\chardef\isacharbraceleft=`\{
+\chardef\isacharbar=`\|
+\chardef\isacharbraceright=`\}
+\chardef\isachartilde=`\~
+
+
+% keyword and section markup
+
+\newcommand{\isakeywordcharunderscore}{\_}
+\newcommand{\isakeyword}[1]
+{\emph{\bf\def\isachardot{.}\def\isacharunderscore{\isakeywordcharunderscore}%
+\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
+\newcommand{\isacommand}[1]{\isakeyword{#1}}
+
+\newcommand{\isamarkupheader}[1]{\section{#1}}
+\newcommand{\isamarkupchapter}[1]{\chapter{#1}}
+\newcommand{\isamarkupsection}[1]{\section{#1}}
+\newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
+\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
+\newcommand{\isamarkupsect}[1]{\section{#1}}
+\newcommand{\isamarkupsubsect}[1]{\subsection{#1}}
+\newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}}
+
+\newif\ifisamarkup
+\newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}
+\newcommand{\isaendpar}{\par\medskip}
+\newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}
+\newenvironment{isamarkuptext}{\isastyletext\begin{isapar}}{\end{isapar}}
+\newenvironment{isamarkuptxt}{\isastyletxt\begin{isapar}}{\end{isapar}}
+\newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
+
+
+% alternative styles
+
+\newcommand{\isabellestyle}{}
+\def\isabellestyle#1{\csname isabellestyle#1\endcsname}
+
+\newcommand{\isabellestylett}{%
+\renewcommand{\isastyle}{\small\tt}%
+\renewcommand{\isastyleminor}{\small\tt}%
+\renewcommand{\isastylescript}{\footnotesize\tt}%
+}
+\newcommand{\isabellestyleit}{%
+\renewcommand{\isastyle}{\small\it}%
+\renewcommand{\isastyleminor}{\it}%
+\renewcommand{\isastylescript}{\footnotesize\it}%
+\renewcommand{\isakeywordcharunderscore}{\mbox{-}}%
+\renewcommand{\isacharbang}{\isamath{!}}%
+\renewcommand{\isachardoublequote}{}%
+\renewcommand{\isacharhash}{\isamath{\#}}%
+\renewcommand{\isachardollar}{\isamath{\$}}%
+\renewcommand{\isacharpercent}{\isamath{\%}}%
+\renewcommand{\isacharampersand}{\isamath{\&}}%
+\renewcommand{\isacharprime}{\isamath{\mskip2mu{'}\mskip-2mu}}%
+\renewcommand{\isacharparenleft}{\isamath{(}}%
+\renewcommand{\isacharparenright}{\isamath{)}}%
+\renewcommand{\isacharasterisk}{\isamath{*}}%
+\renewcommand{\isacharplus}{\isamath{+}}%
+\renewcommand{\isacharcomma}{\isamath{\mathord,}}%
+\renewcommand{\isacharminus}{\isamath{-}}%
+\renewcommand{\isachardot}{\isamath{\mathord.}}%
+\renewcommand{\isacharslash}{\isamath{/}}%
+\renewcommand{\isacharcolon}{\isamath{\mathord:}}%
+\renewcommand{\isacharsemicolon}{\isamath{\mathord;}}%
+\renewcommand{\isacharless}{\isamath{<}}%
+\renewcommand{\isacharequal}{\isamath{=}}%
+\renewcommand{\isachargreater}{\isamath{>}}%
+\renewcommand{\isacharat}{\isamath{@}}%
+\renewcommand{\isacharbrackleft}{\isamath{[}}%
+\renewcommand{\isacharbrackright}{\isamath{]}}%
+\renewcommand{\isacharunderscore}{\mbox{-}}%
+\renewcommand{\isacharbraceleft}{\isamath{\{}}%
+\renewcommand{\isacharbar}{\isamath{\mid}}%
+\renewcommand{\isacharbraceright}{\isamath{\}}}%
+\renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}%
+}
+
+\newcommand{\isabellestylesl}{%
+\isabellestyleit%
+\renewcommand{\isastyle}{\small\sl}%
+\renewcommand{\isastyleminor}{\sl}%
+\renewcommand{\isastylescript}{\footnotesize\sl}%
+}
diff -r 3cc108872aca -r 53022e5f73ff doc-src/IsarTut/generated/isabellesym.sty
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarTut/generated/isabellesym.sty	Wed Jun 05 12:24:14 2002 +0200
@@ -0,0 +1,354 @@
+%%
+%% Author: Markus Wenzel, TU Muenchen
+%% License: GPL (GNU GENERAL PUBLIC LICENSE)
+%%
+%% definitions of standard Isabelle symbols
+%%
+
+% symbol definitions
+
+\newcommand{\isasymzero}{\isatext{\textzerooldstyle}}  %requires textcomp
+\newcommand{\isasymone}{\isatext{\textoneoldstyle}}  %requires textcomp
+\newcommand{\isasymtwo}{\isatext{\texttwooldstyle}}  %requires textcomp
+\newcommand{\isasymthree}{\isatext{\textthreeoldstyle}}  %requires textcomp
+\newcommand{\isasymfour}{\isatext{\textfouroldstyle}}  %requires textcomp
+\newcommand{\isasymfive}{\isatext{\textfiveoldstyle}}  %requires textcomp
+\newcommand{\isasymsix}{\isatext{\textsixoldstyle}}  %requires textcomp
+\newcommand{\isasymseven}{\isatext{\textsevenoldstyle}}  %requires textcomp
+\newcommand{\isasymeight}{\isatext{\texteightoldstyle}}  %requires textcomp
+\newcommand{\isasymnine}{\isatext{\textnineoldstyle}}  %requires textcomp
+\newcommand{\isasymA}{\isamath{\mathcal{A}}}
+\newcommand{\isasymB}{\isamath{\mathcal{B}}}
+\newcommand{\isasymC}{\isamath{\mathcal{C}}}
+\newcommand{\isasymD}{\isamath{\mathcal{D}}}
+\newcommand{\isasymE}{\isamath{\mathcal{E}}}
+\newcommand{\isasymF}{\isamath{\mathcal{F}}}
+\newcommand{\isasymG}{\isamath{\mathcal{G}}}
+\newcommand{\isasymH}{\isamath{\mathcal{H}}}
+\newcommand{\isasymI}{\isamath{\mathcal{I}}}
+\newcommand{\isasymJ}{\isamath{\mathcal{J}}}
+\newcommand{\isasymK}{\isamath{\mathcal{K}}}
+\newcommand{\isasymL}{\isamath{\mathcal{L}}}
+\newcommand{\isasymM}{\isamath{\mathcal{M}}}
+\newcommand{\isasymN}{\isamath{\mathcal{N}}}
+\newcommand{\isasymO}{\isamath{\mathcal{O}}}
+\newcommand{\isasymP}{\isamath{\mathcal{P}}}
+\newcommand{\isasymQ}{\isamath{\mathcal{Q}}}
+\newcommand{\isasymR}{\isamath{\mathcal{R}}}
+\newcommand{\isasymS}{\isamath{\mathcal{S}}}
+\newcommand{\isasymT}{\isamath{\mathcal{T}}}
+\newcommand{\isasymU}{\isamath{\mathcal{U}}}
+\newcommand{\isasymV}{\isamath{\mathcal{V}}}
+\newcommand{\isasymW}{\isamath{\mathcal{W}}}
+\newcommand{\isasymX}{\isamath{\mathcal{X}}}
+\newcommand{\isasymY}{\isamath{\mathcal{Y}}}
+\newcommand{\isasymZ}{\isamath{\mathcal{Z}}}
+\newcommand{\isasyma}{\isamath{\mathrm{a}}}
+\newcommand{\isasymb}{\isamath{\mathrm{b}}}
+\newcommand{\isasymc}{\isamath{\mathrm{c}}}
+\newcommand{\isasymd}{\isamath{\mathrm{d}}}
+\newcommand{\isasyme}{\isamath{\mathrm{e}}}
+\newcommand{\isasymf}{\isamath{\mathrm{f}}}
+\newcommand{\isasymg}{\isamath{\mathrm{g}}}
+\newcommand{\isasymh}{\isamath{\mathrm{h}}}
+\newcommand{\isasymi}{\isamath{\mathrm{i}}}
+\newcommand{\isasymj}{\isamath{\mathrm{j}}}
+\newcommand{\isasymk}{\isamath{\mathrm{k}}}
+\newcommand{\isasyml}{\isamath{\mathrm{l}}}
+\newcommand{\isasymm}{\isamath{\mathrm{m}}}
+\newcommand{\isasymn}{\isamath{\mathrm{n}}}
+\newcommand{\isasymo}{\isamath{\mathrm{o}}}
+\newcommand{\isasymp}{\isamath{\mathrm{p}}}
+\newcommand{\isasymq}{\isamath{\mathrm{q}}}
+\newcommand{\isasymr}{\isamath{\mathrm{r}}}
+\newcommand{\isasyms}{\isamath{\mathrm{s}}}
+\newcommand{\isasymt}{\isamath{\mathrm{t}}}
+\newcommand{\isasymu}{\isamath{\mathrm{u}}}
+\newcommand{\isasymv}{\isamath{\mathrm{v}}}
+\newcommand{\isasymw}{\isamath{\mathrm{w}}}
+\newcommand{\isasymx}{\isamath{\mathrm{x}}}
+\newcommand{\isasymy}{\isamath{\mathrm{y}}}
+\newcommand{\isasymz}{\isamath{\mathrm{z}}}
+\newcommand{\isasymAA}{\isamath{\mathfrak{A}}}  %requires eufrak
+\newcommand{\isasymBB}{\isamath{\mathfrak{B}}}  %requires eufrak
+\newcommand{\isasymCC}{\isamath{\mathfrak{C}}}  %requires eufrak
+\newcommand{\isasymDD}{\isamath{\mathfrak{D}}}  %requires eufrak
+\newcommand{\isasymEE}{\isamath{\mathfrak{E}}}  %requires eufrak
+\newcommand{\isasymFF}{\isamath{\mathfrak{F}}}  %requires eufrak
+\newcommand{\isasymGG}{\isamath{\mathfrak{G}}}  %requires eufrak
+\newcommand{\isasymHH}{\isamath{\mathfrak{H}}}  %requires eufrak
+\newcommand{\isasymII}{\isamath{\mathfrak{I}}}  %requires eufrak
+\newcommand{\isasymJJ}{\isamath{\mathfrak{J}}}  %requires eufrak
+\newcommand{\isasymKK}{\isamath{\mathfrak{K}}}  %requires eufrak
+\newcommand{\isasymLL}{\isamath{\mathfrak{L}}}  %requires eufrak
+\newcommand{\isasymMM}{\isamath{\mathfrak{M}}}  %requires eufrak
+\newcommand{\isasymNN}{\isamath{\mathfrak{N}}}  %requires eufrak
+\newcommand{\isasymOO}{\isamath{\mathfrak{O}}}  %requires eufrak
+\newcommand{\isasymPP}{\isamath{\mathfrak{P}}}  %requires eufrak
+\newcommand{\isasymQQ}{\isamath{\mathfrak{Q}}}  %requires eufrak
+\newcommand{\isasymRR}{\isamath{\mathfrak{R}}}  %requires eufrak
+\newcommand{\isasymSS}{\isamath{\mathfrak{S}}}  %requires eufrak
+\newcommand{\isasymTT}{\isamath{\mathfrak{T}}}  %requires eufrak
+\newcommand{\isasymUU}{\isamath{\mathfrak{U}}}  %requires eufrak
+\newcommand{\isasymVV}{\isamath{\mathfrak{V}}}  %requires eufrak
+\newcommand{\isasymWW}{\isamath{\mathfrak{W}}}  %requires eufrak
+\newcommand{\isasymXX}{\isamath{\mathfrak{X}}}  %requires eufrak
+\newcommand{\isasymYY}{\isamath{\mathfrak{Y}}}  %requires eufrak
+\newcommand{\isasymZZ}{\isamath{\mathfrak{Z}}}  %requires eufrak
+\newcommand{\isasymaa}{\isamath{\mathfrak{a}}}  %requires eufrak
+\newcommand{\isasymbb}{\isamath{\mathfrak{b}}}  %requires eufrak
+\newcommand{\isasymcc}{\isamath{\mathfrak{c}}}  %requires eufrak
+\newcommand{\isasymdd}{\isamath{\mathfrak{d}}}  %requires eufrak
+\newcommand{\isasymee}{\isamath{\mathfrak{e}}}  %requires eufrak
+\newcommand{\isasymff}{\isamath{\mathfrak{f}}}  %requires eufrak
+\newcommand{\isasymgg}{\isamath{\mathfrak{g}}}  %requires eufrak
+\newcommand{\isasymhh}{\isamath{\mathfrak{h}}}  %requires eufrak
+\newcommand{\isasymii}{\isamath{\mathfrak{i}}}  %requires eufrak
+\newcommand{\isasymjj}{\isamath{\mathfrak{j}}}  %requires eufrak
+\newcommand{\isasymkk}{\isamath{\mathfrak{k}}}  %requires eufrak
+\newcommand{\isasymll}{\isamath{\mathfrak{l}}}  %requires eufrak
+\newcommand{\isasymmm}{\isamath{\mathfrak{m}}}  %requires eufrak
+\newcommand{\isasymnn}{\isamath{\mathfrak{n}}}  %requires eufrak
+\newcommand{\isasymoo}{\isamath{\mathfrak{o}}}  %requires eufrak
+\newcommand{\isasympp}{\isamath{\mathfrak{p}}}  %requires eufrak
+\newcommand{\isasymqq}{\isamath{\mathfrak{q}}}  %requires eufrak
+\newcommand{\isasymrr}{\isamath{\mathfrak{r}}}  %requires eufrak
+\newcommand{\isasymss}{\isamath{\mathfrak{s}}}  %requires eufrak
+\newcommand{\isasymtt}{\isamath{\mathfrak{t}}}  %requires eufrak
+\newcommand{\isasymuu}{\isamath{\mathfrak{u}}}  %requires eufrak
+\newcommand{\isasymvv}{\isamath{\mathfrak{v}}}  %requires eufrak
+\newcommand{\isasymww}{\isamath{\mathfrak{w}}}  %requires eufrak
+\newcommand{\isasymxx}{\isamath{\mathfrak{x}}}  %requires eufrak
+\newcommand{\isasymyy}{\isamath{\mathfrak{y}}}  %requires eufrak
+\newcommand{\isasymzz}{\isamath{\mathfrak{z}}}  %requires eufrak
+\newcommand{\isasymalpha}{\isamath{\alpha}}
+\newcommand{\isasymbeta}{\isamath{\beta}}
+\newcommand{\isasymgamma}{\isamath{\gamma}}
+\newcommand{\isasymdelta}{\isamath{\delta}}
+\newcommand{\isasymepsilon}{\isamath{\varepsilon}}
+\newcommand{\isasymzeta}{\isamath{\zeta}}
+\newcommand{\isasymeta}{\isamath{\eta}}
+\newcommand{\isasymtheta}{\isamath{\vartheta}}
+\newcommand{\isasymiota}{\isamath{\iota}}
+\newcommand{\isasymkappa}{\isamath{\kappa}}
+\newcommand{\isasymlambda}{\isamath{\lambda}}
+\newcommand{\isasymmu}{\isamath{\mu}}
+\newcommand{\isasymnu}{\isamath{\nu}}
+\newcommand{\isasymxi}{\isamath{\xi}}
+\newcommand{\isasympi}{\isamath{\pi}}
+\newcommand{\isasymrho}{\isamath{\varrho}}
+\newcommand{\isasymsigma}{\isamath{\sigma}}
+\newcommand{\isasymtau}{\isamath{\tau}}
+\newcommand{\isasymupsilon}{\isamath{\upsilon}}
+\newcommand{\isasymphi}{\isamath{\varphi}}
+\newcommand{\isasymchi}{\isamath{\chi}}
+\newcommand{\isasympsi}{\isamath{\psi}}
+\newcommand{\isasymomega}{\isamath{\omega}}
+\newcommand{\isasymGamma}{\isamath{\Gamma}}
+\newcommand{\isasymDelta}{\isamath{\Delta}}
+\newcommand{\isasymTheta}{\isamath{\Theta}}
+\newcommand{\isasymLambda}{\isamath{\Lambda}}
+\newcommand{\isasymXi}{\isamath{\Xi}}
+\newcommand{\isasymPi}{\isamath{\Pi}}
+\newcommand{\isasymSigma}{\isamath{\Sigma}}
+\newcommand{\isasymUpsilon}{\isamath{\Upsilon}}
+\newcommand{\isasymPhi}{\isamath{\Phi}}
+\newcommand{\isasymPsi}{\isamath{\Psi}}
+\newcommand{\isasymOmega}{\isamath{\Omega}}
+\newcommand{\isasymbool}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{B}}}
+\newcommand{\isasymcomplex}{\isamath{\mathrm{C}\mkern-15mu{\phantom{\mathrm{t}}\vrule}\mkern9mu}}
+\newcommand{\isasymnat}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{N}}}
+\newcommand{\isasymrat}{\isamath{\mathrm{Q}\mkern-16mu{\phantom{\mathrm{t}}\vrule}\mkern10mu}}
+\newcommand{\isasymreal}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{R}}}
+\newcommand{\isasymint}{\isamath{\mathsf{Z}\mkern-7.5mu\mathsf{Z}}}
+\newcommand{\isasymleftarrow}{\isamath{\leftarrow}}
+\newcommand{\isasymlongleftarrow}{\isamath{\longleftarrow}}
+\newcommand{\isasymrightarrow}{\isamath{\rightarrow}}
+\newcommand{\isasymlongrightarrow}{\isamath{\longrightarrow}}
+\newcommand{\isasymLeftarrow}{\isamath{\Leftarrow}}
+\newcommand{\isasymLongleftarrow}{\isamath{\Longleftarrow}}
+\newcommand{\isasymRightarrow}{\isamath{\Rightarrow}}
+\newcommand{\isasymLongrightarrow}{\isamath{\Longrightarrow}}
+\newcommand{\isasymleftrightarrow}{\isamath{\leftrightarrow}}
+\newcommand{\isasymlongleftrightarrow}{\isamath{\longleftrightarrow}}
+\newcommand{\isasymLeftrightarrow}{\isamath{\Leftrightarrow}}
+\newcommand{\isasymLongleftrightarrow}{\isamath{\Longleftrightarrow}}
+\newcommand{\isasymmapsto}{\isamath{\mapsto}}
+\newcommand{\isasymlongmapsto}{\isamath{\longmapsto}}
+\newcommand{\isasymmidarrow}{\isamath{\relbar}}
+\newcommand{\isasymMidarrow}{\isamath{\Relbar}}
+\newcommand{\isasymhookleftarrow}{\isamath{\hookleftarrow}}
+\newcommand{\isasymhookrightarrow}{\isamath{\hookrightarrow}}
+\newcommand{\isasymleftharpoondown}{\isamath{\leftharpoondown}}
+\newcommand{\isasymrightharpoondown}{\isamath{\rightharpoondown}}
+\newcommand{\isasymleftharpoonup}{\isamath{\leftharpoonup}}
+\newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}}
+\newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}}
+\newcommand{\isasymleadsto}{\isamath{\leadsto}}  %requires latexsym
+\newcommand{\isasymup}{\isamath{\uparrow}}
+\newcommand{\isasymUp}{\isamath{\Uparrow}}
+\newcommand{\isasymdown}{\isamath{\downarrow}}
+\newcommand{\isasymDown}{\isamath{\Downarrow}}
+\newcommand{\isasymupdown}{\isamath{\updownarrow}}
+\newcommand{\isasymUpdown}{\isamath{\Updownarrow}}
+\newcommand{\isasymlangle}{\isamath{\langle}}
+\newcommand{\isasymrangle}{\isamath{\rangle}}
+\newcommand{\isasymlceil}{\isamath{\lceil}}
+\newcommand{\isasymrceil}{\isamath{\rceil}}
+\newcommand{\isasymlfloor}{\isamath{\lfloor}}
+\newcommand{\isasymrfloor}{\isamath{\rfloor}}
+\newcommand{\isasymlparr}{\isamath{\mathopen{(\mkern-3mu\mid}}}
+\newcommand{\isasymrparr}{\isamath{\mathclose{\mid\mkern-3mu)}}}
+\newcommand{\isasymlbrakk}{\isamath{\mathopen{\lbrack\mkern-3mu\lbrack}}}
+\newcommand{\isasymrbrakk}{\isamath{\mathclose{\rbrack\mkern-3mu\rbrack}}}
+\newcommand{\isasymlbrace}{\isamath{\mathopen{\lbrace\mkern-4.5mu\mid}}}
+\newcommand{\isasymrbrace}{\isamath{\mathclose{\mid\mkern-4.5mu\rbrace}}}
+\newcommand{\isasymguillemotleft}{\isatext{\flqq}}  %requires babel
+\newcommand{\isasymguillemotright}{\isatext{\frqq}}  %requires babel
+\newcommand{\isasymColon}{\isamath{\mathrel{::}}}
+\newcommand{\isasymnot}{\isamath{\neg}}
+\newcommand{\isasymbottom}{\isamath{\bot}}
+\newcommand{\isasymtop}{\isamath{\top}}
+\newcommand{\isasymand}{\isamath{\wedge}}
+\newcommand{\isasymAnd}{\isamath{\bigwedge}}
+\newcommand{\isasymor}{\isamath{\vee}}
+\newcommand{\isasymOr}{\isamath{\bigvee}}
+\newcommand{\isasymforall}{\isamath{\forall\,}}
+\newcommand{\isasymexists}{\isamath{\exists\,}}
+\newcommand{\isasymbox}{\isamath{\Box}}  %requires latexsym
+\newcommand{\isasymdiamond}{\isamath{\Diamond}}  %requires latexsym
+\newcommand{\isasymturnstile}{\isamath{\vdash}}
+\newcommand{\isasymTurnstile}{\isamath{\models}}
+\newcommand{\isasymtturnstile}{\isamath{\vdash\!\!\!\vdash}}
+\newcommand{\isasymTTurnstile}{\isamath{\mid\!\models}}
+\newcommand{\isasymstileturn}{\isamath{\dashv}}
+\newcommand{\isasymsurd}{\isamath{\surd}}
+\newcommand{\isasymle}{\isamath{\le}}
+\newcommand{\isasymge}{\isamath{\ge}}
+\newcommand{\isasymlless}{\isamath{\ll}}
+\newcommand{\isasymggreater}{\isamath{\gg}}
+\newcommand{\isasymlesssim}{\isamath{\lesssim}}  %requires amssymb
+\newcommand{\isasymgreatersim}{\isamath{\gtrsim}}  %requires amssymb
+\newcommand{\isasymlessapprox}{\isamath{\lessapprox}}  %requires amssymb
+\newcommand{\isasymgreaterapprox}{\isamath{\gtrapprox}}  %requires amssymb
+\newcommand{\isasymin}{\isamath{\in}}
+\newcommand{\isasymnotin}{\isamath{\notin}}
+\newcommand{\isasymsubset}{\isamath{\subset}}
+\newcommand{\isasymsupset}{\isamath{\supset}}
+\newcommand{\isasymsubseteq}{\isamath{\subseteq}}
+\newcommand{\isasymsupseteq}{\isamath{\supseteq}}
+\newcommand{\isasymsqsubset}{\isamath{\sqsubset}}
+\newcommand{\isasymsqsupset}{\isamath{\sqsupset}}  %requires latexsym
+\newcommand{\isasymsqsubseteq}{\isamath{\sqsubseteq}}
+\newcommand{\isasymsqsupseteq}{\isamath{\sqsupseteq}}
+\newcommand{\isasyminter}{\isamath{\cap}}
+\newcommand{\isasymInter}{\isamath{\bigcap\,}}
+\newcommand{\isasymunion}{\isamath{\cup}}
+\newcommand{\isasymUnion}{\isamath{\bigcup\,}}
+\newcommand{\isasymsqunion}{\isamath{\sqcup}}
+\newcommand{\isasymSqunion}{\isamath{\bigsqcup\,}}
+\newcommand{\isasymsqinter}{\isamath{\sqcap}}
+\newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}}  %requires stmaryrd
+\newcommand{\isasymuplus}{\isamath{\uplus}}
+\newcommand{\isasymUplus}{\isamath{\biguplus\,}}
+\newcommand{\isasymnoteq}{\isamath{\not=}}
+\newcommand{\isasymsim}{\isamath{\sim}}
+\newcommand{\isasymdoteq}{\isamath{\doteq}}
+\newcommand{\isasymsimeq}{\isamath{\simeq}}
+\newcommand{\isasymapprox}{\isamath{\approx}}
+\newcommand{\isasymasymp}{\isamath{\asymp}}
+\newcommand{\isasymcong}{\isamath{\cong}}
+\newcommand{\isasymsmile}{\isamath{\smile}}
+\newcommand{\isasymequiv}{\isamath{\equiv}}
+\newcommand{\isasymfrown}{\isamath{\frown}}
+\newcommand{\isasympropto}{\isamath{\propto}}
+\newcommand{\isasymbowtie}{\isamath{\bowtie}}
+\newcommand{\isasymprec}{\isamath{\prec}}
+\newcommand{\isasymsucc}{\isamath{\succ}}
+\newcommand{\isasympreceq}{\isamath{\preceq}}
+\newcommand{\isasymsucceq}{\isamath{\succeq}}
+\newcommand{\isasymparallel}{\isamath{\parallel}}
+\newcommand{\isasymbar}{\isamath{\mid}}
+\newcommand{\isasymplusminus}{\isamath{\pm}}
+\newcommand{\isasymminusplus}{\isamath{\mp}}
+\newcommand{\isasymtimes}{\isamath{\times}}
+\newcommand{\isasymdiv}{\isamath{\div}}
+\newcommand{\isasymcdot}{\isamath{\cdot}}
+\newcommand{\isasymstar}{\isamath{\star}}
+\newcommand{\isasymbullet}{\boldmath\isamath{\mathchoice{\displaystyle{\cdot}}{\textstyle{\cdot}}{\scriptstyle{\bullet}}{\scriptscriptstyle{\bullet}}}}
+\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{\isasymtriangleleft}{\isamath{\triangleleft}}
+\newcommand{\isasymtriangleright}{\isamath{\triangleright}}
+\newcommand{\isasymtriangle}{\isamath{\triangle}}
+\newcommand{\isasymtriangleq}{\isamath{\triangleq}}  %requires amssymb
+\newcommand{\isasymoplus}{\isamath{\oplus}}
+\newcommand{\isasymOplus}{\isamath{\bigoplus\,}}
+\newcommand{\isasymotimes}{\isamath{\otimes}}
+\newcommand{\isasymOtimes}{\isamath{\bigotimes\,}}
+\newcommand{\isasymodot}{\isamath{\odot}}
+\newcommand{\isasymOdot}{\isamath{\bigodot\,}}
+\newcommand{\isasymominus}{\isamath{\ominus}}
+\newcommand{\isasymoslash}{\isamath{\oslash}}
+\newcommand{\isasymdots}{\isamath{\dots}}
+\newcommand{\isasymcdots}{\isamath{\cdots}}
+\newcommand{\isasymSum}{\isamath{\sum\,}}
+\newcommand{\isasymProd}{\isamath{\prod\,}}
+\newcommand{\isasymCoprod}{\isamath{\coprod\,}}
+\newcommand{\isasyminfinity}{\isamath{\infty}}
+\newcommand{\isasymintegral}{\isamath{\int\,}}
+\newcommand{\isasymointegral}{\isamath{\oint\,}}
+\newcommand{\isasymclubsuit}{\isamath{\clubsuit}}
+\newcommand{\isasymdiamondsuit}{\isamath{\diamondsuit}}
+\newcommand{\isasymheartsuit}{\isamath{\heartsuit}}
+\newcommand{\isasymspadesuit}{\isamath{\spadesuit}}
+\newcommand{\isasymaleph}{\isamath{\aleph}}
+\newcommand{\isasymemptyset}{\isamath{\emptyset}}
+\newcommand{\isasymnabla}{\isamath{\nabla}}
+\newcommand{\isasympartial}{\isamath{\partial}}
+\newcommand{\isasymRe}{\isamath{\Re}}
+\newcommand{\isasymIm}{\isamath{\Im}}
+\newcommand{\isasymflat}{\isamath{\flat}}
+\newcommand{\isasymnatural}{\isamath{\natural}}
+\newcommand{\isasymsharp}{\isamath{\sharp}}
+\newcommand{\isasymangle}{\isamath{\angle}}
+\newcommand{\isasymcopyright}{\isatext{\rm\copyright}}
+\newcommand{\isasymregistered}{\isatext{\rm\textregistered}}
+\newcommand{\isasymhyphen}{\isatext{\rm-}}
+\newcommand{\isasyminverse}{\isamath{{}^{-1}}}
+\newcommand{\isasymonesuperior}{\isamath{\mathonesuperior}}  %requires latin1
+\newcommand{\isasymonequarter}{\isatext{\rm\textonequarter}}  %requires latin1
+\newcommand{\isasymtwosuperior}{\isamath{\mathtwosuperior}}  %requires latin1
+\newcommand{\isasymonehalf}{\isatext{\rm\textonehalf}}  %requires latin1
+\newcommand{\isasymthreesuperior}{\isamath{\maththreesuperior}}  %requires latin1
+\newcommand{\isasymthreequarters}{\isatext{\rm\textthreequarters}}  %requires latin1
+\newcommand{\isasymordfeminine}{\isatext{\rm\textordfeminine}}
+\newcommand{\isasymordmasculine}{\isatext{\rm\textordmasculine}}
+\newcommand{\isasymsection}{\isatext{\rm\S}}
+\newcommand{\isasymparagraph}{\isatext{\rm\P}}
+\newcommand{\isasymexclamdown}{\isatext{\rm\textexclamdown}}
+\newcommand{\isasymquestiondown}{\isatext{\rm\textquestiondown}}
+\newcommand{\isasymeuro}{\isatext{\EUR}}  %requires marvosym
+\newcommand{\isasympounds}{\isamath{\pounds}}
+\newcommand{\isasymyen}{\isatext{\yen}}  %requires amssymb
+\newcommand{\isasymcent}{\isatext{\cent}}  %requires wasysym
+\newcommand{\isasymcurrency}{\isatext{\currency}}  %requires wasysym
+\newcommand{\isasymdegree}{\isatext{\rm\textdegree}}  %requires latin1
+\newcommand{\isasymamalg}{\isamath{\amalg}}
+\newcommand{\isasymmho}{\isamath{\mho}}  %requires latexsym
+\newcommand{\isasymlozenge}{\isamath{\lozenge}}  %requires amssym
+\newcommand{\isasymJoin}{\isamath{\Join}}  %requires latexsym
+\newcommand{\isasymwp}{\isamath{\wp}}
+\newcommand{\isasymwrong}{\isamath{\wr}}
+\newcommand{\isasymstruct}{\isamath{\diamond}}
+\newcommand{\isasymacute}{\isatext{\'\relax}}
+\newcommand{\isasymindex}{\isatext{\i}}
+\newcommand{\isasymdieresis}{\isatext{\"\relax}}
+\newcommand{\isasymcedilla}{\isatext{\c\relax}}
+\newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}
+\newcommand{\isasymspacespace}{\isamath{~~}}
diff -r 3cc108872aca -r 53022e5f73ff doc-src/IsarTut/isar-tutorial.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarTut/isar-tutorial.tex	Wed Jun 05 12:24:14 2002 +0200
@@ -0,0 +1,64 @@
+
+\documentclass[12pt,a4paper,fleqn]{report}
+\usepackage{graphicx,../iman,../extra,../isar}
+\usepackage{generated/isabelle,generated/isabellesym}
+\usepackage{../pdfsetup}  % last one!
+
+\isabellestyle{it}
+
+\renewcommand{\isacommand}[1]
+{\ifthenelse{\equal{sorry}{#1}}{$\;$\dummyproof}
+  {\ifthenelse{\equal{oops}{#1}}{$\vdots$}{\isakeyword{#1}}}}
+\newcommand{\idt}[1]{{\mathord{\mathit{#1}}}}
+\newcommand{\DUMMYPROOF}{{\langle\idt{proof}\rangle}}
+\newcommand{\dummyproof}{$\DUMMYPROOF$}
+
+\newcommand{\cmd}[1]{\isacommand{#1}}
+
+\newcommand{\secref}[1]{\S\ref{#1}}
+\newcommand{\figref}[1]{figure~\ref{#1}}
+
+\hyphenation{Isabelle}
+\hyphenation{Isar}
+\hyphenation{Haskell}
+
+\title{\includegraphics[scale=0.5]{isabelle_isar}
+  \\[4ex] The Art of structured proof composition \\ in Isabelle/Isar}
+\author{\emph{Markus Wenzel} \\ TU M\"unchen}
+
+
+\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
+
+\pagestyle{headings}
+\sloppy
+\binperiod     %%%treat . like a binary operator
+
+
+\begin{document}
+
+\underscoreoff
+
+\maketitle
+
+\begin{abstract}
+  FIXME
+\end{abstract}
+
+
+\pagenumbering{roman} \tableofcontents \clearfirst
+
+\input{generated/Tutorial}
+
+\begingroup
+  \bibliographystyle{plain} \small\raggedright\frenchspacing
+  \bibliography{../manual}
+\endgroup
+
+\nocite{Wenzel-PhD}
+
+\end{document}
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: t
+%%% End: