superceded by IsarOverview

--- a/doc-src/IsarTut/IsaMakefile	Sat Apr 30 14:18:36 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,34 +0,0 @@
-
-## 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

--- a/doc-src/IsarTut/Makefile	Sat Apr 30 14:18:36 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,38 +0,0 @@
-#
-# $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)

--- a/doc-src/IsarTut/Tutorial/ROOT.ML	Sat Apr 30 14:18:36 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,4 +0,0 @@
-
-set quick_and_dirty;
-
-use_thy "Tutorial";

--- a/doc-src/IsarTut/Tutorial/Tutorial.thy	Sat Apr 30 14:18:36 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,349 +0,0 @@
-
-(*<*)
-theory Tutorial = Main:
-(*>*)
-
-chapter {* Introduction *}
-
-chapter {* Technical issues *}
-
-section {* Source texts *}
-
-section {* Interaction and debugging *}
-
-section {* Step-by-step examples *}
-
-subsection {* Summing natural numbers *}
-
-theorem "2 * (\<Sum>i < n + 1. i) = n * (n + 1)"  (is "?P n")
-proof (induct n)
-  case 0
-  then show "?P 0" by simp
-next
-  case (Suc n)
-  let "?S n = _" = "?P n"
-  have "?S (n + 1) = ?S n + 2 * (n + 1)" by simp
-  also have "?S n = n * (n + 1)" .
-  also have "\<dots> + 2 * (n + 1) = (n + 1) * (n + 2)" by simp
-  finally show "?P (Suc n)" by simp
-qed
-
-theorem "2 * (\<Sum>i < n + 1. i) = n * (n + 1)"
-proof (induct n)
-  case 0
-  then show ?case by simp
-next
-  case Suc
-  then show ?case by simp
-qed
-
-theorem "2 * (\<Sum>i < n + 1. i) = n * (n + 1)"
-  by (induct n) simp_all
-    
-theorem "2 * (\<Sum>i < n + 1. i) = n * (n + 1)"
-  apply (induct n)
-   apply simp_all
-  done
-
-
-
-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
-(*>*)

--- a/doc-src/IsarTut/Tutorial/document/Tutorial.tex	Sat Apr 30 14:18:36 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,687 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{Tutorial}%
-\isamarkupfalse%
-%
-\isamarkupchapter{Introduction%
-}
-\isamarkuptrue%
-%
-\isamarkupsection{Step-by-step examples%
-}
-\isamarkuptrue%
-%
-\isamarkupsubsection{Summing natural numbers%
-}
-\isamarkuptrue%
-\isacommand{theorem}\ {\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
-\isamarkupfalse%
-\isacommand{proof}\ {\isacharparenleft}induct\ n{\isacharparenright}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{case}\ {\isadigit{0}}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{then}\ \isamarkupfalse%
-\isacommand{show}\ {\isachardoublequote}{\isacharquery}P\ {\isadigit{0}}{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{by}\ simp\isanewline
-\isamarkupfalse%
-\isacommand{next}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{case}\ {\isacharparenleft}Suc\ n{\isacharparenright}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{let}\ {\isachardoublequote}{\isacharquery}S\ n\ {\isacharequal}\ {\isacharunderscore}{\isachardoublequote}\ {\isacharequal}\ {\isachardoublequote}{\isacharquery}P\ n{\isachardoublequote}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{have}\ {\isachardoublequote}{\isacharquery}S\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharequal}\ {\isacharquery}S\ n\ {\isacharplus}\ {\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{by}\ simp\isanewline
-\ \ \isamarkupfalse%
-\isacommand{also}\ \isamarkupfalse%
-\isacommand{have}\ {\isachardoublequote}{\isacharquery}S\ n\ {\isacharequal}\ n\ {\isacharasterisk}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{{\isachardot}}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{also}\ \isamarkupfalse%
-\isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isacharplus}\ {\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{2}}{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{by}\ simp\isanewline
-\ \ \isamarkupfalse%
-\isacommand{finally}\ \isamarkupfalse%
-\isacommand{show}\ {\isachardoublequote}{\isacharquery}P\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{by}\ simp\isanewline
-\isamarkupfalse%
-\isacommand{qed}\isanewline
-\isanewline
-\isamarkupfalse%
-\isacommand{theorem}\ {\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
-\isamarkupfalse%
-\isacommand{proof}\ {\isacharparenleft}induct\ n{\isacharparenright}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{case}\ {\isadigit{0}}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{then}\ \isamarkupfalse%
-\isacommand{show}\ {\isacharquery}case\ \isamarkupfalse%
-\isacommand{by}\ simp\isanewline
-\isamarkupfalse%
-\isacommand{next}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{case}\ Suc\isanewline
-\ \ \isamarkupfalse%
-\isacommand{then}\ \isamarkupfalse%
-\isacommand{show}\ {\isacharquery}case\ \isamarkupfalse%
-\isacommand{by}\ simp\isanewline
-\isamarkupfalse%
-\isacommand{qed}\isanewline
-\isanewline
-\isamarkupfalse%
-\isacommand{theorem}\ {\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
-\ \ \isamarkupfalse%
-\isacommand{by}\ {\isacharparenleft}induct\ n{\isacharparenright}\ simp{\isacharunderscore}all\isanewline
-\ \ \ \ \isanewline
-\isamarkupfalse%
-\isacommand{theorem}\ {\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
-\ \ \isamarkupfalse%
-\isacommand{apply}\ {\isacharparenleft}induct\ n{\isacharparenright}\isanewline
-\ \ \ \isamarkupfalse%
-\isacommand{apply}\ simp{\isacharunderscore}all\isanewline
-\ \ \isamarkupfalse%
-\isacommand{done}\isamarkupfalse%
-%
-\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:

--- a/doc-src/IsarTut/Tutorial/document/isabelle.sty	Sat Apr 30 14:18:36 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,156 +0,0 @@
-%%
-%% Author: Markus Wenzel, TU Muenchen
-%%
-%% 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}%
-}

--- a/doc-src/IsarTut/Tutorial/document/isabellesym.sty	Sat Apr 30 14:18:36 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,353 +0,0 @@
-%%
-%% Author: Markus Wenzel, TU Muenchen
-%%
-%% 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{~~}}

--- a/doc-src/IsarTut/Tutorial/document/root.tex	Sat Apr 30 14:18:36 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,6 +0,0 @@
-
-\documentclass{article}
-
-\begin{document}
---- dummy ---
-\end{document}

--- a/doc-src/IsarTut/generated/Tutorial.tex	Sat Apr 30 14:18:36 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,620 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{Tutorial}%
-\isamarkupfalse%
-%
-\isamarkupchapter{Introduction%
-}
-\isamarkuptrue%
-%
-\isamarkupchapter{Technical issues%
-}
-\isamarkuptrue%
-%
-\isamarkupsection{Source texts%
-}
-\isamarkuptrue%
-%
-\isamarkupsection{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:

--- a/doc-src/IsarTut/generated/isabelle.sty	Sat Apr 30 14:18:36 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,156 +0,0 @@
-%%
-%% Author: Markus Wenzel, TU Muenchen
-%%
-%% 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}%
-}

--- a/doc-src/IsarTut/generated/isabellesym.sty	Sat Apr 30 14:18:36 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,353 +0,0 @@
-%%
-%% Author: Markus Wenzel, TU Muenchen
-%%
-%% 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{~~}}

--- a/doc-src/IsarTut/isar-tutorial.tex	Sat Apr 30 14:18:36 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,64 +0,0 @@
-
-\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: