1.1 --- a/doc-src/TutorialI/Datatype/Fundata.thy	Tue Aug 29 15:43:29 2000 +0200
     1.2 +++ b/doc-src/TutorialI/Datatype/Fundata.thy	Tue Aug 29 16:05:13 2000 +0200
     1.3 @@ -41,12 +41,12 @@
     1.4  text{*\noindent
     1.5  but it is worth taking a look at the proof state after the induction step
     1.6  to understand what the presence of the function type entails:
     1.7 -\begin{isabellepar}%
     1.8 +\begin{isabelle}
     1.9  ~1.~map\_bt~g~(map\_bt~f~Tip)~=~map\_bt~(g~{\isasymcirc}~f)~Tip\isanewline
    1.10  ~2.~{\isasymAnd}a~F.\isanewline
    1.11  ~~~~~~{\isasymforall}x.~map\_bt~g~(map\_bt~f~(F~x))~=~map\_bt~(g~{\isasymcirc}~f)~(F~x)~{\isasymLongrightarrow}\isanewline
    1.12  ~~~~~~map\_bt~g~(map\_bt~f~(Branch~a~F))~=~map\_bt~(g~{\isasymcirc}~f)~(Branch~a~F)%
    1.13 -\end{isabellepar}%
    1.14 +\end{isabelle}
    1.15  *}
    1.16  (*<*)
    1.17  end

     2.1 --- a/doc-src/TutorialI/Datatype/document/Fundata.tex	Tue Aug 29 15:43:29 2000 +0200
     2.2 +++ b/doc-src/TutorialI/Datatype/document/Fundata.tex	Tue Aug 29 16:05:13 2000 +0200
     2.3 @@ -43,12 +43,12 @@
     2.4  \noindent
     2.5  but it is worth taking a look at the proof state after the induction step
     2.6  to understand what the presence of the function type entails:
     2.7 -\begin{isabellepar}%
     2.8 +\begin{isabelle}
     2.9  ~1.~map\_bt~g~(map\_bt~f~Tip)~=~map\_bt~(g~{\isasymcirc}~f)~Tip\isanewline
    2.10  ~2.~{\isasymAnd}a~F.\isanewline
    2.11  ~~~~~~{\isasymforall}x.~map\_bt~g~(map\_bt~f~(F~x))~=~map\_bt~(g~{\isasymcirc}~f)~(F~x)~{\isasymLongrightarrow}\isanewline
    2.12  ~~~~~~map\_bt~g~(map\_bt~f~(Branch~a~F))~=~map\_bt~(g~{\isasymcirc}~f)~(Branch~a~F)%
    2.13 -\end{isabellepar}%%
    2.14 +\end{isabelle}%
    2.15  \end{isamarkuptext}%
    2.16  \end{isabellebody}%
    2.17  %%% Local Variables:

     3.1 --- a/doc-src/TutorialI/Misc/AdvancedInd.thy	Tue Aug 29 15:43:29 2000 +0200
     3.2 +++ b/doc-src/TutorialI/Misc/AdvancedInd.thy	Tue Aug 29 16:05:13 2000 +0200
     3.3 @@ -28,13 +28,13 @@
     3.4  Induction variable occurs also among premises!
     3.5  \end{quote}
     3.6  and leads to the base case
     3.7 -\begin{isabellepar}%
     3.8 +\begin{isabelle}
     3.9  \ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ (rev\ [])\ =\ last\ []
    3.10 -\end{isabellepar}%
    3.11 +\end{isabelle}
    3.12  which, after simplification, becomes
    3.13 -\begin{isabellepar}%
    3.14 +\begin{isabelle}
    3.15  \ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ []\ =\ last\ []
    3.16 -\end{isabellepar}%
    3.17 +\end{isabelle}
    3.18  We cannot prove this equality because we do not know what \isa{hd} and
    3.19  \isa{last} return when applied to \isa{[]}.
    3.20  
    3.21 @@ -56,9 +56,9 @@
    3.22  
    3.23  text{*\noindent
    3.24  This time, induction leaves us with the following base case
    3.25 -\begin{isabellepar}%
    3.26 +\begin{isabelle}
    3.27  \ 1.\ []\ {\isasymnoteq}\ []\ {\isasymlongrightarrow}\ hd\ (rev\ [])\ =\ last\ []
    3.28 -\end{isabellepar}%
    3.29 +\end{isabelle}
    3.30  which is trivial, and \isa{auto} finishes the whole proof.
    3.31  
    3.32  If \isa{hd\_rev} is meant to be a simplification rule, you are done. But if you
    3.33 @@ -169,18 +169,18 @@
    3.34  (*>*)
    3.35  txt{*\noindent
    3.36  which leaves us with the following proof state:
    3.37 -\begin{isabellepar}%
    3.38 +\begin{isabelle}
    3.39  \ 1.\ {\isasymAnd}\mbox{n}.\ {\isasymforall}\mbox{m}.\ \mbox{m}\ <\ \mbox{n}\ {\isasymlongrightarrow}\ ({\isasymforall}\mbox{i}.\ \mbox{m}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i})\isanewline
    3.40  \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymforall}\mbox{i}.\ \mbox{n}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i}
    3.41 -\end{isabellepar}%
    3.42 +\end{isabelle}
    3.43  After stripping the \isa{\isasymforall i}, the proof continues with a case
    3.44  distinction on \isa{i}. The case \isa{i = 0} is trivial and we focus on the
    3.45  other case:
    3.46 -\begin{isabellepar}%
    3.47 +\begin{isabelle}
    3.48  \ 1.\ {\isasymAnd}\mbox{n}\ \mbox{i}\ \mbox{nat}.\isanewline
    3.49  \ \ \ \ \ \ \ {\isasymlbrakk}{\isasymforall}\mbox{m}.\ \mbox{m}\ <\ \mbox{n}\ {\isasymlongrightarrow}\ ({\isasymforall}\mbox{i}.\ \mbox{m}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i});\ \mbox{i}\ =\ Suc\ \mbox{nat}{\isasymrbrakk}\isanewline
    3.50  \ \ \ \ \ \ \ {\isasymLongrightarrow}\ \mbox{n}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i}
    3.51 -\end{isabellepar}%
    3.52 +\end{isabelle}
    3.53  *};
    3.54  
    3.55  by(blast intro!: f_ax Suc_leI intro:le_less_trans);

     4.1 --- a/doc-src/TutorialI/Misc/Itrev.thy	Tue Aug 29 15:43:29 2000 +0200
     4.2 +++ b/doc-src/TutorialI/Misc/Itrev.thy	Tue Aug 29 16:05:13 2000 +0200
     4.3 @@ -32,9 +32,9 @@
     4.4  
     4.5  txt{*\noindent
     4.6  Unfortunately, this is not a complete success:
     4.7 -\begin{isabellepar}%
     4.8 +\begin{isabelle}
     4.9  ~1.~\dots~itrev~list~[]~=~rev~list~{\isasymLongrightarrow}~itrev~list~[a]~=~rev~list~@~[a]%
    4.10 -\end{isabellepar}%
    4.11 +\end{isabelle}
    4.12  Just as predicted above, the overall goal, and hence the induction
    4.13  hypothesis, is too weak to solve the induction step because of the fixed
    4.14  \isa{[]}. The corresponding heuristic:
    4.15 @@ -59,11 +59,11 @@
    4.16  Although we now have two variables, only \isa{xs} is suitable for
    4.17  induction, and we repeat our above proof attempt. Unfortunately, we are still
    4.18  not there:
    4.19 -\begin{isabellepar}%
    4.20 +\begin{isabelle}
    4.21  ~1.~{\isasymAnd}a~list.\isanewline
    4.22  ~~~~~~~itrev~list~ys~=~rev~list~@~ys~{\isasymLongrightarrow}\isanewline
    4.23  ~~~~~~~itrev~list~(a~\#~ys)~=~rev~list~@~a~\#~ys%
    4.24 -\end{isabellepar}%
    4.25 +\end{isabelle}
    4.26  The induction hypothesis is still too weak, but this time it takes no
    4.27  intuition to generalize: the problem is that \isa{ys} is fixed throughout
    4.28  the subgoal, but the induction hypothesis needs to be applied with

     5.1 --- a/doc-src/TutorialI/Misc/case_splits.thy	Tue Aug 29 15:43:29 2000 +0200
     5.2 +++ b/doc-src/TutorialI/Misc/case_splits.thy	Tue Aug 29 16:05:13 2000 +0200
     5.3 @@ -11,9 +11,9 @@
     5.4  
     5.5  txt{*\noindent
     5.6  can be split into
     5.7 -\begin{isabellepar}%
     5.8 +\begin{isabelle}
     5.9  ~1.~{\isasymforall}xs.~(xs~=~[]~{\isasymlongrightarrow}~rev~xs~=~[])~{\isasymand}~(xs~{\isasymnoteq}~[]~{\isasymlongrightarrow}~rev~xs~{\isasymnoteq}~[])%
    5.10 -\end{isabellepar}%
    5.11 +\end{isabelle}
    5.12  by a degenerate form of simplification
    5.13  *}
    5.14  
    5.15 @@ -34,10 +34,10 @@
    5.16  lemma "(case xs of [] \\<Rightarrow> zs | y#ys \\<Rightarrow> y#(ys@zs)) = xs@zs";
    5.17  txt{*\noindent
    5.18  becomes
    5.19 -\begin{isabellepar}%
    5.20 +\begin{isabelle}
    5.21  ~1.~(xs~=~[]~{\isasymlongrightarrow}~zs~=~xs~@~zs)~{\isasymand}\isanewline
    5.22  ~~~~({\isasymforall}a~list.~xs~=~a~\#~list~{\isasymlongrightarrow}~a~\#~list~@~zs~=~xs~@~zs)%
    5.23 -\end{isabellepar}%
    5.24 +\end{isabelle}
    5.25  by typing
    5.26  *}
    5.27  

     6.1 --- a/doc-src/TutorialI/Misc/def_rewr.thy	Tue Aug 29 15:43:29 2000 +0200
     6.2 +++ b/doc-src/TutorialI/Misc/def_rewr.thy	Tue Aug 29 16:05:13 2000 +0200
     6.3 @@ -28,9 +28,9 @@
     6.4  
     6.5  txt{*\noindent
     6.6  In this particular case, the resulting goal
     6.7 -\begin{isabellepar}%
     6.8 +\begin{isabelle}
     6.9  ~1.~A~{\isasymand}~{\isasymnot}~{\isasymnot}~A~{\isasymor}~{\isasymnot}~A~{\isasymand}~{\isasymnot}~A%
    6.10 -\end{isabellepar}%
    6.11 +\end{isabelle}
    6.12  can be proved by simplification. Thus we could have proved the lemma outright
    6.13  *}(*<*)oops;lemma "exor A (\\<not>A)";(*>*)
    6.14  by(simp add: exor_def)

     7.1 --- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Tue Aug 29 15:43:29 2000 +0200
     7.2 +++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Tue Aug 29 16:05:13 2000 +0200
     7.3 @@ -27,13 +27,13 @@
     7.4  Induction variable occurs also among premises!
     7.5  \end{quote}
     7.6  and leads to the base case
     7.7 -\begin{isabellepar}%
     7.8 +\begin{isabelle}
     7.9  \ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ (rev\ [])\ =\ last\ []
    7.10 -\end{isabellepar}%
    7.11 +\end{isabelle}
    7.12  which, after simplification, becomes
    7.13 -\begin{isabellepar}%
    7.14 +\begin{isabelle}
    7.15  \ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ []\ =\ last\ []
    7.16 -\end{isabellepar}%
    7.17 +\end{isabelle}
    7.18  We cannot prove this equality because we do not know what \isa{hd} and
    7.19  \isa{last} return when applied to \isa{[]}.
    7.20  
    7.21 @@ -51,9 +51,9 @@
    7.22  \begin{isamarkuptext}%
    7.23  \noindent
    7.24  This time, induction leaves us with the following base case
    7.25 -\begin{isabellepar}%
    7.26 +\begin{isabelle}
    7.27  \ 1.\ []\ {\isasymnoteq}\ []\ {\isasymlongrightarrow}\ hd\ (rev\ [])\ =\ last\ []
    7.28 -\end{isabellepar}%
    7.29 +\end{isabelle}
    7.30  which is trivial, and \isa{auto} finishes the whole proof.
    7.31  
    7.32  If \isa{hd\_rev} is meant to be a simplification rule, you are done. But if you
    7.33 @@ -151,18 +151,18 @@
    7.34  \begin{isamarkuptxt}%
    7.35  \noindent
    7.36  which leaves us with the following proof state:
    7.37 -\begin{isabellepar}%
    7.38 +\begin{isabelle}
    7.39  \ 1.\ {\isasymAnd}\mbox{n}.\ {\isasymforall}\mbox{m}.\ \mbox{m}\ <\ \mbox{n}\ {\isasymlongrightarrow}\ ({\isasymforall}\mbox{i}.\ \mbox{m}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i})\isanewline
    7.40  \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymforall}\mbox{i}.\ \mbox{n}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i}
    7.41 -\end{isabellepar}%
    7.42 +\end{isabelle}
    7.43  After stripping the \isa{\isasymforall i}, the proof continues with a case
    7.44  distinction on \isa{i}. The case \isa{i = 0} is trivial and we focus on the
    7.45  other case:
    7.46 -\begin{isabellepar}%
    7.47 +\begin{isabelle}
    7.48  \ 1.\ {\isasymAnd}\mbox{n}\ \mbox{i}\ \mbox{nat}.\isanewline
    7.49  \ \ \ \ \ \ \ {\isasymlbrakk}{\isasymforall}\mbox{m}.\ \mbox{m}\ <\ \mbox{n}\ {\isasymlongrightarrow}\ ({\isasymforall}\mbox{i}.\ \mbox{m}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i});\ \mbox{i}\ =\ Suc\ \mbox{nat}{\isasymrbrakk}\isanewline
    7.50  \ \ \ \ \ \ \ {\isasymLongrightarrow}\ \mbox{n}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i}
    7.51 -\end{isabellepar}%%
    7.52 +\end{isabelle}%
    7.53  \end{isamarkuptxt}%
    7.54  \isacommand{by}{\isacharparenleft}blast\ intro{\isacharbang}{\isacharcolon}\ f{\isacharunderscore}ax\ Suc{\isacharunderscore}leI\ intro{\isacharcolon}le{\isacharunderscore}less{\isacharunderscore}trans{\isacharparenright}%
    7.55  \begin{isamarkuptext}%

     8.1 --- a/doc-src/TutorialI/Misc/document/Itrev.tex	Tue Aug 29 15:43:29 2000 +0200
     8.2 +++ b/doc-src/TutorialI/Misc/document/Itrev.tex	Tue Aug 29 16:05:13 2000 +0200
     8.3 @@ -31,9 +31,9 @@
     8.4  \begin{isamarkuptxt}%
     8.5  \noindent
     8.6  Unfortunately, this is not a complete success:
     8.7 -\begin{isabellepar}%
     8.8 +\begin{isabelle}
     8.9  ~1.~\dots~itrev~list~[]~=~rev~list~{\isasymLongrightarrow}~itrev~list~[a]~=~rev~list~@~[a]%
    8.10 -\end{isabellepar}%
    8.11 +\end{isabelle}
    8.12  Just as predicted above, the overall goal, and hence the induction
    8.13  hypothesis, is too weak to solve the induction step because of the fixed
    8.14  \isa{[]}. The corresponding heuristic:
    8.15 @@ -57,11 +57,11 @@
    8.16  Although we now have two variables, only \isa{xs} is suitable for
    8.17  induction, and we repeat our above proof attempt. Unfortunately, we are still
    8.18  not there:
    8.19 -\begin{isabellepar}%
    8.20 +\begin{isabelle}
    8.21  ~1.~{\isasymAnd}a~list.\isanewline
    8.22  ~~~~~~~itrev~list~ys~=~rev~list~@~ys~{\isasymLongrightarrow}\isanewline
    8.23  ~~~~~~~itrev~list~(a~\#~ys)~=~rev~list~@~a~\#~ys%
    8.24 -\end{isabellepar}%
    8.25 +\end{isabelle}
    8.26  The induction hypothesis is still too weak, but this time it takes no
    8.27  intuition to generalize: the problem is that \isa{ys} is fixed throughout
    8.28  the subgoal, but the induction hypothesis needs to be applied with

     9.1 --- a/doc-src/TutorialI/Misc/document/case_splits.tex	Tue Aug 29 15:43:29 2000 +0200
     9.2 +++ b/doc-src/TutorialI/Misc/document/case_splits.tex	Tue Aug 29 16:05:13 2000 +0200
     9.3 @@ -9,9 +9,9 @@
     9.4  \begin{isamarkuptxt}%
     9.5  \noindent
     9.6  can be split into
     9.7 -\begin{isabellepar}%
     9.8 +\begin{isabelle}
     9.9  ~1.~{\isasymforall}xs.~(xs~=~[]~{\isasymlongrightarrow}~rev~xs~=~[])~{\isasymand}~(xs~{\isasymnoteq}~[]~{\isasymlongrightarrow}~rev~xs~{\isasymnoteq}~[])%
    9.10 -\end{isabellepar}%
    9.11 +\end{isabelle}
    9.12  by a degenerate form of simplification%
    9.13  \end{isamarkuptxt}%
    9.14  \isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ split{\isacharunderscore}if{\isacharparenright}%
    9.15 @@ -30,10 +30,10 @@
    9.16  \begin{isamarkuptxt}%
    9.17  \noindent
    9.18  becomes
    9.19 -\begin{isabellepar}%
    9.20 +\begin{isabelle}
    9.21  ~1.~(xs~=~[]~{\isasymlongrightarrow}~zs~=~xs~@~zs)~{\isasymand}\isanewline
    9.22  ~~~~({\isasymforall}a~list.~xs~=~a~\#~list~{\isasymlongrightarrow}~a~\#~list~@~zs~=~xs~@~zs)%
    9.23 -\end{isabellepar}%
    9.24 +\end{isabelle}
    9.25  by typing%
    9.26  \end{isamarkuptxt}%
    9.27  \isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}%

    10.1 --- a/doc-src/TutorialI/Misc/document/def_rewr.tex	Tue Aug 29 15:43:29 2000 +0200
    10.2 +++ b/doc-src/TutorialI/Misc/document/def_rewr.tex	Tue Aug 29 16:05:13 2000 +0200
    10.3 @@ -26,9 +26,9 @@
    10.4  \begin{isamarkuptxt}%
    10.5  \noindent
    10.6  In this particular case, the resulting goal
    10.7 -\begin{isabellepar}%
    10.8 +\begin{isabelle}
    10.9  ~1.~A~{\isasymand}~{\isasymnot}~{\isasymnot}~A~{\isasymor}~{\isasymnot}~A~{\isasymand}~{\isasymnot}~A%
   10.10 -\end{isabellepar}%
   10.11 +\end{isabelle}
   10.12  can be proved by simplification. Thus we could have proved the lemma outright%
   10.13  \end{isamarkuptxt}%
   10.14  \isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ exor{\isacharunderscore}def{\isacharparenright}%

    11.1 --- a/doc-src/TutorialI/Recdef/Induction.thy	Tue Aug 29 15:43:29 2000 +0200
    11.2 +++ b/doc-src/TutorialI/Recdef/Induction.thy	Tue Aug 29 16:05:13 2000 +0200
    11.3 @@ -31,13 +31,13 @@
    11.4  txt{*\noindent
    11.5  The resulting proof state has three subgoals corresponding to the three
    11.6  clauses for \isa{sep}:
    11.7 -\begin{isabellepar}%
    11.8 +\begin{isabelle}
    11.9  ~1.~{\isasymAnd}a.~map~f~(sep~(a,~[]))~=~sep~(f~a,~map~f~[])\isanewline
   11.10  ~2.~{\isasymAnd}a~x.~map~f~(sep~(a,~[x]))~=~sep~(f~a,~map~f~[x])\isanewline
   11.11  ~3.~{\isasymAnd}a~x~y~zs.\isanewline
   11.12  ~~~~~~~map~f~(sep~(a,~y~\#~zs))~=~sep~(f~a,~map~f~(y~\#~zs))~{\isasymLongrightarrow}\isanewline
   11.13  ~~~~~~~map~f~(sep~(a,~x~\#~y~\#~zs))~=~sep~(f~a,~map~f~(x~\#~y~\#~zs))%
   11.14 -\end{isabellepar}%
   11.15 +\end{isabelle}
   11.16  The rest is pure simplification:
   11.17  *}
   11.18  
   11.19 @@ -57,12 +57,12 @@
   11.20  name of a function that takes an $n$-tuple. Usually the subgoal will
   11.21  contain the term $f~x@1~\dots~x@n$ but this need not be the case. The
   11.22  induction rules do not mention $f$ at all. For example \isa{sep.induct}
   11.23 -\begin{isabellepar}%
   11.24 +\begin{isabelle}
   11.25  {\isasymlbrakk}~{\isasymAnd}a.~P~a~[];\isanewline
   11.26  ~~{\isasymAnd}a~x.~P~a~[x];\isanewline
   11.27  ~~{\isasymAnd}a~x~y~zs.~P~a~(y~\#~zs)~{\isasymLongrightarrow}~P~a~(x~\#~y~\#~zs){\isasymrbrakk}\isanewline
   11.28  {\isasymLongrightarrow}~P~u~v%
   11.29 -\end{isabellepar}%
   11.30 +\end{isabelle}
   11.31  merely says that in order to prove a property \isa{P} of \isa{u} and
   11.32  \isa{v} you need to prove it for the three cases where \isa{v} is the
   11.33  empty list, the singleton list, and the list with at least two elements

    12.1 --- a/doc-src/TutorialI/Recdef/document/Induction.tex	Tue Aug 29 15:43:29 2000 +0200
    12.2 +++ b/doc-src/TutorialI/Recdef/document/Induction.tex	Tue Aug 29 16:05:13 2000 +0200
    12.3 @@ -28,13 +28,13 @@
    12.4  \noindent
    12.5  The resulting proof state has three subgoals corresponding to the three
    12.6  clauses for \isa{sep}:
    12.7 -\begin{isabellepar}%
    12.8 +\begin{isabelle}
    12.9  ~1.~{\isasymAnd}a.~map~f~(sep~(a,~[]))~=~sep~(f~a,~map~f~[])\isanewline
   12.10  ~2.~{\isasymAnd}a~x.~map~f~(sep~(a,~[x]))~=~sep~(f~a,~map~f~[x])\isanewline
   12.11  ~3.~{\isasymAnd}a~x~y~zs.\isanewline
   12.12  ~~~~~~~map~f~(sep~(a,~y~\#~zs))~=~sep~(f~a,~map~f~(y~\#~zs))~{\isasymLongrightarrow}\isanewline
   12.13  ~~~~~~~map~f~(sep~(a,~x~\#~y~\#~zs))~=~sep~(f~a,~map~f~(x~\#~y~\#~zs))%
   12.14 -\end{isabellepar}%
   12.15 +\end{isabelle}
   12.16  The rest is pure simplification:%
   12.17  \end{isamarkuptxt}%
   12.18  \isacommand{by}\ simp{\isacharunderscore}all%
   12.19 @@ -52,12 +52,12 @@
   12.20  name of a function that takes an $n$-tuple. Usually the subgoal will
   12.21  contain the term $f~x@1~\dots~x@n$ but this need not be the case. The
   12.22  induction rules do not mention $f$ at all. For example \isa{sep.induct}
   12.23 -\begin{isabellepar}%
   12.24 +\begin{isabelle}
   12.25  {\isasymlbrakk}~{\isasymAnd}a.~P~a~[];\isanewline
   12.26  ~~{\isasymAnd}a~x.~P~a~[x];\isanewline
   12.27  ~~{\isasymAnd}a~x~y~zs.~P~a~(y~\#~zs)~{\isasymLongrightarrow}~P~a~(x~\#~y~\#~zs){\isasymrbrakk}\isanewline
   12.28  {\isasymLongrightarrow}~P~u~v%
   12.29 -\end{isabellepar}%
   12.30 +\end{isabelle}
   12.31  merely says that in order to prove a property \isa{P} of \isa{u} and
   12.32  \isa{v} you need to prove it for the three cases where \isa{v} is the
   12.33  empty list, the singleton list, and the list with at least two elements

    13.1 --- a/doc-src/TutorialI/ToyList/ToyList.thy	Tue Aug 29 15:43:29 2000 +0200
    13.2 +++ b/doc-src/TutorialI/ToyList/ToyList.thy	Tue Aug 29 16:05:13 2000 +0200
    13.3 @@ -137,24 +137,24 @@
    13.4  The name and the simplification attribute are optional.
    13.5  \end{itemize}
    13.6  Isabelle's response is to print
    13.7 -\begin{isabellepar}%
    13.8 +\begin{isabelle}
    13.9  proof(prove):~step~0\isanewline
   13.10  \isanewline
   13.11  goal~(theorem~rev\_rev):\isanewline
   13.12  rev~(rev~xs)~=~xs\isanewline
   13.13  ~1.~rev~(rev~xs)~=~xs
   13.14 -\end{isabellepar}%
   13.15 +\end{isabelle}
   13.16  The first three lines tell us that we are 0 steps into the proof of
   13.17  theorem \isa{rev_rev}; for compactness reasons we rarely show these
   13.18  initial lines in this tutorial. The remaining lines display the current
   13.19  proof state.
   13.20  Until we have finished a proof, the proof state always looks like this:
   13.21 -\begin{isabellepar}%
   13.22 +\begin{isabelle}
   13.23  $G$\isanewline
   13.24  ~1.~$G\sb{1}$\isanewline
   13.25  ~~\vdots~~\isanewline
   13.26  ~$n$.~$G\sb{n}$
   13.27 -\end{isabellepar}%
   13.28 +\end{isabelle}
   13.29  where $G$
   13.30  is the overall goal that we are trying to prove, and the numbered lines
   13.31  contain the subgoals $G\sb{1}$, \dots, $G\sb{n}$ that we need to prove to
   13.32 @@ -175,15 +175,15 @@
   13.33  By default, induction acts on the first subgoal. The new proof state contains
   13.34  two subgoals, namely the base case (\isa{Nil}) and the induction step
   13.35  (\isa{Cons}):
   13.36 -\begin{isabellepar}%
   13.37 +\begin{isabelle}
   13.38  ~1.~rev~(rev~[])~=~[]\isanewline
   13.39  ~2.~{\isasymAnd}a~list.~rev(rev~list)~=~list~{\isasymLongrightarrow}~rev(rev(a~\#~list))~=~a~\#~list%
   13.40 -\end{isabellepar}%
   13.41 +\end{isabelle}
   13.42  
   13.43  The induction step is an example of the general format of a subgoal:
   13.44 -\begin{isabellepar}%
   13.45 +\begin{isabelle}
   13.46  ~$i$.~{\indexboldpos{\isasymAnd}{$IsaAnd}}$x\sb{1}$~\dots~$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion}
   13.47 -\end{isabellepar}%
   13.48 +\end{isabelle}
   13.49  The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be
   13.50  ignored most of the time, or simply treated as a list of variables local to
   13.51  this subgoal. Their deeper significance is explained in \S\ref{sec:PCproofs}.
   13.52 @@ -208,18 +208,18 @@
   13.53  ``simplify'' the subgoals.  In our case, subgoal~1 is solved completely (thanks
   13.54  to the equation \isa{rev [] = []}) and disappears; the simplified version
   13.55  of subgoal~2 becomes the new subgoal~1:
   13.56 -\begin{isabellepar}%
   13.57 +\begin{isabelle}
   13.58  ~1.~\dots~rev(rev~list)~=~list~{\isasymLongrightarrow}~rev(rev~list~@~a~\#~[])~=~a~\#~list
   13.59 -\end{isabellepar}%
   13.60 +\end{isabelle}
   13.61  In order to simplify this subgoal further, a lemma suggests itself.
   13.62  *}
   13.63  (*<*)
   13.64  oops
   13.65  (*>*)
   13.66  
   13.67 +subsubsection{*First lemma: \texttt{rev(xs \at~ys) = (rev ys) \at~(rev xs)}*}
   13.68 +
   13.69  text{*
   13.70 -\subsubsection*{First lemma: \texttt{rev(xs \at~ys) = (rev ys) \at~(rev xs)}}
   13.71 -
   13.72  After abandoning the above proof attempt\indexbold{abandon
   13.73  proof}\indexbold{proof!abandon} (at the shell level type
   13.74  \isacommand{oops}\indexbold{*oops}) we start a new proof:
   13.75 @@ -247,10 +247,10 @@
   13.76  apply(auto);
   13.77  
   13.78  txt{*
   13.79 -\begin{isabellepar}%
   13.80 +\begin{isabelle}
   13.81  ~1.~rev~ys~=~rev~ys~@~[]\isanewline
   13.82  ~2. \dots
   13.83 -\end{isabellepar}%
   13.84 +\end{isabelle}
   13.85  Again, we need to abandon this proof attempt and prove another simple lemma first.
   13.86  In the future the step of abandoning an incomplete proof before embarking on
   13.87  the proof of a lemma usually remains implicit.
   13.88 @@ -259,9 +259,9 @@
   13.89  oops
   13.90  (*>*)
   13.91  
   13.92 +subsubsection{*Second lemma: \texttt{xs \at~[] = xs}*}
   13.93 +
   13.94  text{*
   13.95 -\subsubsection*{Second lemma: \texttt{xs \at~[] = xs}}
   13.96 -
   13.97  This time the canonical proof procedure
   13.98  *}
   13.99  
  13.100 @@ -272,10 +272,10 @@
  13.101  txt{*
  13.102  \noindent
  13.103  leads to the desired message \isa{No subgoals!}:
  13.104 -\begin{isabellepar}%
  13.105 +\begin{isabelle}
  13.106  xs~@~[]~=~xs\isanewline
  13.107  No~subgoals!
  13.108 -\end{isabellepar}%
  13.109 +\end{isabelle}
  13.110  
  13.111  We still need to confirm that the proof is now finished:
  13.112  *}
  13.113 @@ -302,29 +302,27 @@
  13.114  \noindent
  13.115  we find that this time \isa{auto} solves the base case, but the
  13.116  induction step merely simplifies to
  13.117 -\begin{isabellepar}
  13.118 +\begin{isabelle}
  13.119  ~1.~{\isasymAnd}a~list.\isanewline
  13.120  ~~~~~~~rev~(list~@~ys)~=~rev~ys~@~rev~list~{\isasymLongrightarrow}\isanewline
  13.121  ~~~~~~~(rev~ys~@~rev~list)~@~a~\#~[]~=~rev~ys~@~rev~list~@~a~\#~[]
  13.122 -\end{isabellepar}%
  13.123 +\end{isabelle}
  13.124  Now we need to remember that \isa{\at} associates to the right, and that
  13.125  \isa{\#} and \isa{\at} have the same priority (namely the \isa{65}
  13.126  in their \isacommand{infixr} annotation). Thus the conclusion really is
  13.127 -\begin{isabellepar}%
  13.128 +\begin{isabelle}
  13.129  ~~~~~(rev~ys~@~rev~list)~@~(a~\#~[])~=~rev~ys~@~(rev~list~@~(a~\#~[]))%
  13.130 -\end{isabellepar}%
  13.131 +\end{isabelle}
  13.132  and the missing lemma is associativity of \isa{\at}.
  13.133 +*}
  13.134 +(*<*)oops(*>*)
  13.135  
  13.136 -\subsubsection*{Third lemma: \texttt{(xs \at~ys) \at~zs = xs \at~(ys \at~zs)}}
  13.137 +subsubsection{*Third lemma: \texttt{(xs \at~ys) \at~zs = xs \at~(ys \at~zs)}*}
  13.138  
  13.139 +text{*
  13.140  Abandoning the previous proof, the canonical proof procedure
  13.141  *}
  13.142  
  13.143 -
  13.144 -txt_raw{*\begin{comment}*}
  13.145 -oops
  13.146 -text_raw{*\end{comment}*}
  13.147 -
  13.148  lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)";
  13.149  apply(induct_tac xs);
  13.150  by(auto);
  13.151 @@ -332,7 +330,6 @@
  13.152  text{*
  13.153  \noindent
  13.154  succeeds without further ado.
  13.155 -
  13.156  Now we can go back and prove the first lemma
  13.157  *}
  13.158  

    14.1 --- a/doc-src/TutorialI/ToyList/document/ToyList.tex	Tue Aug 29 15:43:29 2000 +0200
    14.2 +++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Tue Aug 29 16:05:13 2000 +0200
    14.3 @@ -132,24 +132,24 @@
    14.4  The name and the simplification attribute are optional.
    14.5  \end{itemize}
    14.6  Isabelle's response is to print
    14.7 -\begin{isabellepar}%
    14.8 +\begin{isabelle}
    14.9  proof(prove):~step~0\isanewline
   14.10  \isanewline
   14.11  goal~(theorem~rev\_rev):\isanewline
   14.12  rev~(rev~xs)~=~xs\isanewline
   14.13  ~1.~rev~(rev~xs)~=~xs
   14.14 -\end{isabellepar}%
   14.15 +\end{isabelle}
   14.16  The first three lines tell us that we are 0 steps into the proof of
   14.17  theorem \isa{rev_rev}; for compactness reasons we rarely show these
   14.18  initial lines in this tutorial. The remaining lines display the current
   14.19  proof state.
   14.20  Until we have finished a proof, the proof state always looks like this:
   14.21 -\begin{isabellepar}%
   14.22 +\begin{isabelle}
   14.23  $G$\isanewline
   14.24  ~1.~$G\sb{1}$\isanewline
   14.25  ~~\vdots~~\isanewline
   14.26  ~$n$.~$G\sb{n}$
   14.27 -\end{isabellepar}%
   14.28 +\end{isabelle}
   14.29  where $G$
   14.30  is the overall goal that we are trying to prove, and the numbered lines
   14.31  contain the subgoals $G\sb{1}$, \dots, $G\sb{n}$ that we need to prove to
   14.32 @@ -169,15 +169,15 @@
   14.33  By default, induction acts on the first subgoal. The new proof state contains
   14.34  two subgoals, namely the base case (\isa{Nil}) and the induction step
   14.35  (\isa{Cons}):
   14.36 -\begin{isabellepar}%
   14.37 +\begin{isabelle}
   14.38  ~1.~rev~(rev~[])~=~[]\isanewline
   14.39  ~2.~{\isasymAnd}a~list.~rev(rev~list)~=~list~{\isasymLongrightarrow}~rev(rev(a~\#~list))~=~a~\#~list%
   14.40 -\end{isabellepar}%
   14.41 +\end{isabelle}
   14.42  
   14.43  The induction step is an example of the general format of a subgoal:
   14.44 -\begin{isabellepar}%
   14.45 +\begin{isabelle}
   14.46  ~$i$.~{\indexboldpos{\isasymAnd}{$IsaAnd}}$x\sb{1}$~\dots~$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion}
   14.47 -\end{isabellepar}%
   14.48 +\end{isabelle}
   14.49  The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be
   14.50  ignored most of the time, or simply treated as a list of variables local to
   14.51  this subgoal. Their deeper significance is explained in \S\ref{sec:PCproofs}.
   14.52 @@ -200,15 +200,15 @@
   14.53  ``simplify'' the subgoals.  In our case, subgoal~1 is solved completely (thanks
   14.54  to the equation \isa{rev [] = []}) and disappears; the simplified version
   14.55  of subgoal~2 becomes the new subgoal~1:
   14.56 -\begin{isabellepar}%
   14.57 +\begin{isabelle}
   14.58  ~1.~\dots~rev(rev~list)~=~list~{\isasymLongrightarrow}~rev(rev~list~@~a~\#~[])~=~a~\#~list
   14.59 -\end{isabellepar}%
   14.60 +\end{isabelle}
   14.61  In order to simplify this subgoal further, a lemma suggests itself.%
   14.62  \end{isamarkuptxt}%
   14.63  %
   14.64 +\isamarkupsubsubsection{First lemma: \texttt{rev(xs \at~ys) = (rev ys) \at~(rev xs)}}
   14.65 +%
   14.66  \begin{isamarkuptext}%
   14.67 -\subsubsection*{First lemma: \texttt{rev(xs \at~ys) = (rev ys) \at~(rev xs)}}
   14.68 -
   14.69  After abandoning the above proof attempt\indexbold{abandon
   14.70  proof}\indexbold{proof!abandon} (at the shell level type
   14.71  \isacommand{oops}\indexbold{*oops}) we start a new proof:%
   14.72 @@ -232,18 +232,18 @@
   14.73  \end{isamarkuptxt}%
   14.74  \isacommand{apply}{\isacharparenleft}auto{\isacharparenright}%
   14.75  \begin{isamarkuptxt}%
   14.76 -\begin{isabellepar}%
   14.77 +\begin{isabelle}
   14.78  ~1.~rev~ys~=~rev~ys~@~[]\isanewline
   14.79  ~2. \dots
   14.80 -\end{isabellepar}%
   14.81 +\end{isabelle}
   14.82  Again, we need to abandon this proof attempt and prove another simple lemma first.
   14.83  In the future the step of abandoning an incomplete proof before embarking on
   14.84  the proof of a lemma usually remains implicit.%
   14.85  \end{isamarkuptxt}%
   14.86  %
   14.87 +\isamarkupsubsubsection{Second lemma: \texttt{xs \at~[] = xs}}
   14.88 +%
   14.89  \begin{isamarkuptext}%
   14.90 -\subsubsection*{Second lemma: \texttt{xs \at~[] = xs}}
   14.91 -
   14.92  This time the canonical proof procedure%
   14.93  \end{isamarkuptext}%
   14.94  \isacommand{lemma}\ app{\isacharunderscore}Nil\isadigit{2}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline
   14.95 @@ -252,10 +252,10 @@
   14.96  \begin{isamarkuptxt}%
   14.97  \noindent
   14.98  leads to the desired message \isa{No subgoals!}:
   14.99 -\begin{isabellepar}%
  14.100 +\begin{isabelle}
  14.101  xs~@~[]~=~xs\isanewline
  14.102  No~subgoals!
  14.103 -\end{isabellepar}%
  14.104 +\end{isabelle}
  14.105  
  14.106  We still need to confirm that the proof is now finished:%
  14.107  \end{isamarkuptxt}%
  14.108 @@ -279,34 +279,31 @@
  14.109  \noindent
  14.110  we find that this time \isa{auto} solves the base case, but the
  14.111  induction step merely simplifies to
  14.112 -\begin{isabellepar}
  14.113 +\begin{isabelle}
  14.114  ~1.~{\isasymAnd}a~list.\isanewline
  14.115  ~~~~~~~rev~(list~@~ys)~=~rev~ys~@~rev~list~{\isasymLongrightarrow}\isanewline
  14.116  ~~~~~~~(rev~ys~@~rev~list)~@~a~\#~[]~=~rev~ys~@~rev~list~@~a~\#~[]
  14.117 -\end{isabellepar}%
  14.118 +\end{isabelle}
  14.119  Now we need to remember that \isa{\at} associates to the right, and that
  14.120  \isa{\#} and \isa{\at} have the same priority (namely the \isa{65}
  14.121  in their \isacommand{infixr} annotation). Thus the conclusion really is
  14.122 -\begin{isabellepar}%
  14.123 +\begin{isabelle}
  14.124  ~~~~~(rev~ys~@~rev~list)~@~(a~\#~[])~=~rev~ys~@~(rev~list~@~(a~\#~[]))%
  14.125 -\end{isabellepar}%
  14.126 -and the missing lemma is associativity of \isa{\at}.
  14.127 -
  14.128 -\subsubsection*{Third lemma: \texttt{(xs \at~ys) \at~zs = xs \at~(ys \at~zs)}}
  14.129 -
  14.130 -Abandoning the previous proof, the canonical proof procedure%
  14.131 +\end{isabelle}
  14.132 +and the missing lemma is associativity of \isa{\at}.%
  14.133  \end{isamarkuptxt}%
  14.134  %
  14.135 -\begin{comment}
  14.136 -\isacommand{oops}%
  14.137 -\end{comment}
  14.138 +\isamarkupsubsubsection{Third lemma: \texttt{(xs \at~ys) \at~zs = xs \at~(ys \at~zs)}}
  14.139 +%
  14.140 +\begin{isamarkuptext}%
  14.141 +Abandoning the previous proof, the canonical proof procedure%
  14.142 +\end{isamarkuptext}%
  14.143  \isacommand{lemma}\ app{\isacharunderscore}assoc\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharat}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ {\isacharparenleft}ys\ {\isacharat}\ zs{\isacharparenright}{\isachardoublequote}\isanewline
  14.144  \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
  14.145  \isacommand{by}{\isacharparenleft}auto{\isacharparenright}%
  14.146  \begin{isamarkuptext}%
  14.147  \noindent
  14.148  succeeds without further ado.
  14.149 -
  14.150  Now we can go back and prove the first lemma%
  14.151  \end{isamarkuptext}%
  14.152  \isacommand{lemma}\ rev{\isacharunderscore}app\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}rev\ ys{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isachardoublequote}\isanewline

    15.1 --- a/doc-src/TutorialI/Trie/Trie.thy	Tue Aug 29 15:43:29 2000 +0200
    15.2 +++ b/doc-src/TutorialI/Trie/Trie.thy	Tue Aug 29 16:05:13 2000 +0200
    15.3 @@ -109,11 +109,11 @@
    15.4  
    15.5  txt{*\noindent
    15.6  Unfortunately, this time we are left with three intimidating looking subgoals:
    15.7 -\begin{isabellepar}%
    15.8 +\begin{isabelle}
    15.9  ~1.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs\isanewline
   15.10  ~2.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs\isanewline
   15.11  ~3.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs%
   15.12 -\end{isabellepar}%
   15.13 +\end{isabelle}
   15.14  Clearly, if we want to make headway we have to instantiate \isa{bs} as
   15.15  well now. It turns out that instead of induction, case distinction
   15.16  suffices:

    16.1 --- a/doc-src/TutorialI/Trie/document/Trie.tex	Tue Aug 29 15:43:29 2000 +0200
    16.2 +++ b/doc-src/TutorialI/Trie/document/Trie.tex	Tue Aug 29 16:05:13 2000 +0200
    16.3 @@ -98,11 +98,11 @@
    16.4  \begin{isamarkuptxt}%
    16.5  \noindent
    16.6  Unfortunately, this time we are left with three intimidating looking subgoals:
    16.7 -\begin{isabellepar}%
    16.8 +\begin{isabelle}
    16.9  ~1.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs\isanewline
   16.10  ~2.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs\isanewline
   16.11  ~3.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs%
   16.12 -\end{isabellepar}%
   16.13 +\end{isabelle}
   16.14  Clearly, if we want to make headway we have to instantiate \isa{bs} as
   16.15  well now. It turns out that instead of induction, case distinction
   16.16  suffices:%

    17.1 --- a/doc-src/TutorialI/tutorial.tex	Tue Aug 29 15:43:29 2000 +0200
    17.2 +++ b/doc-src/TutorialI/tutorial.tex	Tue Aug 29 16:05:13 2000 +0200
    17.3 @@ -4,8 +4,6 @@
    17.4  \usepackage{latexsym,verbatim,graphicx,../iman,../extra,../ttbox,comment}
    17.5  \usepackage{../pdfsetup}    %last package!
    17.6  
    17.7 -\newcommand\Out[1]{\texttt{\textsl{#1}}}   %% for output from terminal sessions
    17.8 -
    17.9  %\newtheorem{theorem}{Theorem}[section]
   17.10  \newtheorem{Exercise}{Exercise}[section]
   17.11  \newenvironment{exercise}{\begin{Exercise}\rm}{\end{Exercise}}
   17.12 @@ -22,7 +20,6 @@
   17.13  \newcommand{\isasymFun}{\isasymRightarrow}
   17.14  \newcommand{\isasymuniqex}{\emph{$\exists!\,$}}
   17.15  
   17.16 -\newenvironment{isabellepar}{\medskip\begin{isabelle}}{\end{isabelle}\medskip}
   17.17  \renewenvironment{isamarkuptxt}{\begin{isamarkuptext}}{\end{isamarkuptext}}
   17.18  
   17.19  %%% to index derived rls:  ^\([a-zA-Z0-9][a-zA-Z0-9_]*\)        \\tdx{\1}