*** empty log message ***
authornipkow
Tue Aug 29 15:13:10 2000 +0200 (2000-08-29)
changeset 97217e51c9f3d5a0
parent 9720 3b7b72db57f1
child 9722 a5f86aed785b
*** empty log message ***
TFL/tfl.sml
doc-src/Tutorial/fp.tex
doc-src/TutorialI/CodeGen/document/CodeGen.tex
doc-src/TutorialI/Datatype/document/ABexpr.tex
doc-src/TutorialI/Datatype/document/Fundata.tex
doc-src/TutorialI/Datatype/document/Nested.tex
doc-src/TutorialI/Datatype/document/unfoldnested.tex
doc-src/TutorialI/Ifexpr/document/Ifexpr.tex
doc-src/TutorialI/IsaMakefile
doc-src/TutorialI/Misc/ROOT.ML
doc-src/TutorialI/Misc/case_splits.thy
doc-src/TutorialI/Misc/cases.thy
doc-src/TutorialI/Misc/document/AdvancedInd.tex
doc-src/TutorialI/Misc/document/Itrev.tex
doc-src/TutorialI/Misc/document/Tree.tex
doc-src/TutorialI/Misc/document/Tree2.tex
doc-src/TutorialI/Misc/document/arith1.tex
doc-src/TutorialI/Misc/document/arith2.tex
doc-src/TutorialI/Misc/document/arith3.tex
doc-src/TutorialI/Misc/document/arith4.tex
doc-src/TutorialI/Misc/document/asm_simp.tex
doc-src/TutorialI/Misc/document/case_splits.tex
doc-src/TutorialI/Misc/document/cases.tex
doc-src/TutorialI/Misc/document/cond_rewr.tex
doc-src/TutorialI/Misc/document/def_rewr.tex
doc-src/TutorialI/Misc/document/fakenat.tex
doc-src/TutorialI/Misc/document/let_rewr.tex
doc-src/TutorialI/Misc/document/natsum.tex
doc-src/TutorialI/Misc/document/pairs.tex
doc-src/TutorialI/Misc/document/prime_def.tex
doc-src/TutorialI/Misc/document/trace_simp.tex
doc-src/TutorialI/Misc/document/types.tex
doc-src/TutorialI/Recdef/Nested2.thy
doc-src/TutorialI/Recdef/document/Induction.tex
doc-src/TutorialI/Recdef/document/Nested0.tex
doc-src/TutorialI/Recdef/document/Nested1.tex
doc-src/TutorialI/Recdef/document/Nested2.tex
doc-src/TutorialI/Recdef/document/examples.tex
doc-src/TutorialI/Recdef/document/simplification.tex
doc-src/TutorialI/Recdef/document/termination.tex
doc-src/TutorialI/ToyList/document/ToyList.tex
doc-src/TutorialI/Trie/document/Option2.tex
doc-src/TutorialI/Trie/document/Trie.tex
doc-src/TutorialI/fp.tex
src/Provers/classical.ML
src/Pure/library.ML
src/Pure/term.ML
src/Pure/thm.ML
     1.1 --- a/TFL/tfl.sml	Tue Aug 29 12:28:48 2000 +0200
     1.2 +++ b/TFL/tfl.sml	Tue Aug 29 15:13:10 2000 +0200
     1.3 @@ -47,9 +47,8 @@
     1.4  
     1.5  fun add_cong(congs,thm) =
     1.6    let val c = cong_hd thm
     1.7 -  in case assoc(congs,c) of None => (c,thm)::congs
     1.8 -     | _ => (warning ("Overwriting congruence rule for " ^ quote c);
     1.9 -             overwrite (congs, (c,thm)))
    1.10 +  in overwrite_warn (congs,(c,thm))
    1.11 +       ("Overwriting congruence rule for " ^ quote c)
    1.12    end
    1.13  
    1.14  fun del_cong(congs,thm) =
     2.1 --- a/doc-src/Tutorial/fp.tex	Tue Aug 29 12:28:48 2000 +0200
     2.2 +++ b/doc-src/Tutorial/fp.tex	Tue Aug 29 15:13:10 2000 +0200
     2.3 @@ -1029,7 +1029,7 @@
     2.4  Nevertheless the simplifier can be instructed to perform \texttt{case}-splits
     2.5  by adding the appropriate rule to the simpset:
     2.6  \begin{ttbox}
     2.7 -by(simp_tac (simpset() addsplits [split_list_case]) 1);
     2.8 +by(simp_tac (simpset() addsplits [list.split]) 1);
     2.9  \end{ttbox}\indexbold{*addsplits}
    2.10  solves the initial goal outright, which \texttt{Simp_tac} alone will not do.
    2.11  
     3.1 --- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex	Tue Aug 29 12:28:48 2000 +0200
     3.2 +++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex	Tue Aug 29 15:13:10 2000 +0200
     3.3 @@ -1,5 +1,4 @@
     3.4 -%
     3.5 -\begin{isabellebody}%
     3.6 +\begin{isabelle}%
     3.7  %
     3.8  \begin{isamarkuptext}%
     3.9  \noindent
    3.10 @@ -112,7 +111,7 @@
    3.11  However, this is unnecessary because the generalized version fully subsumes
    3.12  its instance.%
    3.13  \end{isamarkuptext}%
    3.14 -\end{isabellebody}%
    3.15 +\end{isabelle}%
    3.16  %%% Local Variables:
    3.17  %%% mode: latex
    3.18  %%% TeX-master: "root"
     4.1 --- a/doc-src/TutorialI/Datatype/document/ABexpr.tex	Tue Aug 29 12:28:48 2000 +0200
     4.2 +++ b/doc-src/TutorialI/Datatype/document/ABexpr.tex	Tue Aug 29 15:13:10 2000 +0200
     4.3 @@ -1,5 +1,4 @@
     4.4 -%
     4.5 -\begin{isabellebody}%
     4.6 +\begin{isabelle}%
     4.7  %
     4.8  \begin{isamarkuptext}%
     4.9  Sometimes it is necessary to define two datatypes that depend on each
    4.10 @@ -112,7 +111,7 @@
    4.11    it.  ({\em Hint:} proceed as in \S\ref{sec:boolex}).
    4.12  \end{exercise}%
    4.13  \end{isamarkuptext}%
    4.14 -\end{isabellebody}%
    4.15 +\end{isabelle}%
    4.16  %%% Local Variables:
    4.17  %%% mode: latex
    4.18  %%% TeX-master: "root"
     5.1 --- a/doc-src/TutorialI/Datatype/document/Fundata.tex	Tue Aug 29 12:28:48 2000 +0200
     5.2 +++ b/doc-src/TutorialI/Datatype/document/Fundata.tex	Tue Aug 29 15:13:10 2000 +0200
     5.3 @@ -1,5 +1,4 @@
     5.4 -%
     5.5 -\begin{isabellebody}%
     5.6 +\begin{isabelle}%
     5.7  \isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree\ {\isacharequal}\ Tip\ {\isacharbar}\ Branch\ {\isacharprime}a\ {\isachardoublequote}{\isacharprime}i\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree{\isachardoublequote}%
     5.8  \begin{isamarkuptext}%
     5.9  \noindent Parameter \isa{'a} is the type of values stored in
    5.10 @@ -50,7 +49,7 @@
    5.11  ~~~~~~map\_bt~g~(map\_bt~f~(Branch~a~F))~=~map\_bt~(g~{\isasymcirc}~f)~(Branch~a~F)%
    5.12  \end{isabellepar}%%
    5.13  \end{isamarkuptext}%
    5.14 -\end{isabellebody}%
    5.15 +\end{isabelle}%
    5.16  %%% Local Variables:
    5.17  %%% mode: latex
    5.18  %%% TeX-master: "root"
     6.1 --- a/doc-src/TutorialI/Datatype/document/Nested.tex	Tue Aug 29 12:28:48 2000 +0200
     6.2 +++ b/doc-src/TutorialI/Datatype/document/Nested.tex	Tue Aug 29 15:13:10 2000 +0200
     6.3 @@ -1,5 +1,4 @@
     6.4 -%
     6.5 -\begin{isabellebody}%
     6.6 +\begin{isabelle}%
     6.7  %
     6.8  \begin{isamarkuptext}%
     6.9  So far, all datatypes had the property that on the right-hand side of their
    6.10 @@ -122,7 +121,7 @@
    6.11  constructor \isa{Sum} in \S\ref{sec:datatype-mut-rec} could take a list of
    6.12  expressions as its argument: \isa{Sum "'a aexp list"}.%
    6.13  \end{isamarkuptext}%
    6.14 -\end{isabellebody}%
    6.15 +\end{isabelle}%
    6.16  %%% Local Variables:
    6.17  %%% mode: latex
    6.18  %%% TeX-master: "root"
     7.1 --- a/doc-src/TutorialI/Datatype/document/unfoldnested.tex	Tue Aug 29 12:28:48 2000 +0200
     7.2 +++ b/doc-src/TutorialI/Datatype/document/unfoldnested.tex	Tue Aug 29 15:13:10 2000 +0200
     7.3 @@ -1,7 +1,6 @@
     7.4 -%
     7.5 -\begin{isabellebody}%
     7.6 +\begin{isabelle}%
     7.7  \isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}{\isachardoublequote}term{\isachardoublequote}\ {\isacharequal}\ Var\ {\isacharprime}a\ {\isacharbar}\ App\ {\isacharprime}b\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharunderscore}list{\isachardoublequote}\isanewline
     7.8 -\isakeyword{and}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharunderscore}list\ {\isacharequal}\ Nil\ {\isacharbar}\ Cons\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isachardoublequote}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharunderscore}list{\isachardoublequote}\end{isabellebody}%
     7.9 +\isakeyword{and}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharunderscore}list\ {\isacharequal}\ Nil\ {\isacharbar}\ Cons\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isachardoublequote}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharunderscore}list{\isachardoublequote}\end{isabelle}%
    7.10  %%% Local Variables:
    7.11  %%% mode: latex
    7.12  %%% TeX-master: "root"
     8.1 --- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Tue Aug 29 12:28:48 2000 +0200
     8.2 +++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Tue Aug 29 15:13:10 2000 +0200
     8.3 @@ -1,5 +1,4 @@
     8.4 -%
     8.5 -\begin{isabellebody}%
     8.6 +\begin{isabelle}%
     8.7  %
     8.8  \begin{isamarkuptext}%
     8.9  \subsubsection{How can we model boolean expressions?}
    8.10 @@ -132,7 +131,7 @@
    8.11  and prove \isa{normal(norm b)}. Of course, this requires a lemma about
    8.12  normality of \isa{normif}:%
    8.13  \end{isamarkuptext}%
    8.14 -\isacommand{lemma}{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ normal{\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}normal\ t\ {\isasymand}\ normal\ e{\isacharparenright}{\isachardoublequote}\end{isabellebody}%
    8.15 +\isacommand{lemma}{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ normal{\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}normal\ t\ {\isasymand}\ normal\ e{\isacharparenright}{\isachardoublequote}\end{isabelle}%
    8.16  %%% Local Variables:
    8.17  %%% mode: latex
    8.18  %%% TeX-master: "root"
     9.1 --- a/doc-src/TutorialI/IsaMakefile	Tue Aug 29 12:28:48 2000 +0200
     9.2 +++ b/doc-src/TutorialI/IsaMakefile	Tue Aug 29 15:13:10 2000 +0200
     9.3 @@ -98,7 +98,8 @@
     9.4  HOL-Misc: HOL $(LOG)/HOL-Misc.gz
     9.5  
     9.6  $(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/Tree2.thy Misc/cases.thy \
     9.7 -  Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy Misc/types.thy Misc/prime_def.thy \
     9.8 +  Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy Misc/types.thy \
     9.9 +  Misc/prime_def.thy Misc/case_exprs.thy \
    9.10    Misc/arith1.thy Misc/arith2.thy Misc/arith3.thy Misc/arith4.thy \
    9.11    Misc/def_rewr.thy Misc/let_rewr.thy Misc/cond_rewr.thy Misc/case_splits.thy \
    9.12    Misc/trace_simp.thy Misc/Itrev.thy Misc/AdvancedInd.thy Misc/asm_simp.thy
    10.1 --- a/doc-src/TutorialI/Misc/ROOT.ML	Tue Aug 29 12:28:48 2000 +0200
    10.2 +++ b/doc-src/TutorialI/Misc/ROOT.ML	Tue Aug 29 15:13:10 2000 +0200
    10.3 @@ -1,6 +1,7 @@
    10.4  use_thy "Tree";
    10.5  use_thy "Tree2";
    10.6  use_thy "cases";
    10.7 +use_thy "case_exprs";
    10.8  use_thy "fakenat";
    10.9  use_thy "natsum";
   10.10  use_thy "arith1";
    11.1 --- a/doc-src/TutorialI/Misc/case_splits.thy	Tue Aug 29 12:28:48 2000 +0200
    11.2 +++ b/doc-src/TutorialI/Misc/case_splits.thy	Tue Aug 29 15:13:10 2000 +0200
    11.3 @@ -81,6 +81,27 @@
    11.4  *}
    11.5  lemmas [split del] = list.split;
    11.6  
    11.7 +text{*
    11.8 +The above split rules intentionally only affect the conclusion of a
    11.9 +subgoal.  If you want to split an \isa{if} or \isa{case}-expression in
   11.10 +the assumptions, you have to apply \isa{split\_if\_asm} or $t$\isa{.split_asm}:
   11.11 +*}
   11.12 +
   11.13 +lemma "if xs = [] then ys ~= [] else ys = [] ==> xs @ ys ~= []"
   11.14 +apply(simp only: split: split_if_asm);
   11.15 +
   11.16 +txt{*\noindent
   11.17 +In contrast to splitting the conclusion, this actually creates two
   11.18 +separate subgoals (which are solved by \isa{simp\_all}):
   11.19 +\begin{isabelle}
   11.20 +\ \isadigit{1}{\isachardot}\ {\isasymlbrakk}\mbox{xs}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ \mbox{ys}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ \mbox{ys}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\isanewline
   11.21 +\ \isadigit{2}{\isachardot}\ {\isasymlbrakk}\mbox{xs}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ \mbox{ys}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ \mbox{xs}\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}
   11.22 +\end{isabelle}
   11.23 +If you need to split both in the assumptions and the conclusion,
   11.24 +use $t$\isa{.splits} which subsumes $t$\isa{.split} and $t$\isa{.split_asm}.
   11.25 +*}
   11.26 +
   11.27  (*<*)
   11.28 +by(simp_all)
   11.29  end
   11.30  (*>*)
    12.1 --- a/doc-src/TutorialI/Misc/cases.thy	Tue Aug 29 12:28:48 2000 +0200
    12.2 +++ b/doc-src/TutorialI/Misc/cases.thy	Tue Aug 29 15:13:10 2000 +0200
    12.3 @@ -2,6 +2,19 @@
    12.4  theory "cases" = Main:;
    12.5  (*>*)
    12.6  
    12.7 +subsection{*Structural induction and case distinction*}
    12.8 +
    12.9 +text{*
   12.10 +\indexbold{structural induction}
   12.11 +\indexbold{induction!structural}
   12.12 +\indexbold{case distinction}
   12.13 +Almost all the basic laws about a datatype are applied automatically during
   12.14 +simplification. Only induction is invoked by hand via \isaindex{induct_tac},
   12.15 +which works for any datatype. In some cases, induction is overkill and a case
   12.16 +distinction over all constructors of the datatype suffices. This is performed
   12.17 +by \isaindexbold{case_tac}. A trivial example:
   12.18 +*}
   12.19 +
   12.20  lemma "(case xs of [] \\<Rightarrow> [] | y#ys \\<Rightarrow> xs) = xs";
   12.21  apply(case_tac xs);
   12.22  
   12.23 @@ -14,8 +27,13 @@
   12.24  which is solved automatically:
   12.25  *}
   12.26  
   12.27 -by(auto);
   12.28 -(**)
   12.29 +by(auto)
   12.30 +
   12.31 +text{*
   12.32 +Note that we do not need to give a lemma a name if we do not intend to refer
   12.33 +to it explicitly in the future.
   12.34 +*}
   12.35 +
   12.36  (*<*)
   12.37  end
   12.38  (*>*)
    13.1 --- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Tue Aug 29 12:28:48 2000 +0200
    13.2 +++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Tue Aug 29 15:13:10 2000 +0200
    13.3 @@ -1,5 +1,4 @@
    13.4 -%
    13.5 -\begin{isabellebody}%
    13.6 +\begin{isabelle}%
    13.7  %
    13.8  \begin{isamarkuptext}%
    13.9  \noindent
   13.10 @@ -272,7 +271,7 @@
   13.11  For example \isa{less\_induct} is the special case where \isa{r} is \isa{<} on \isa{nat}.
   13.12  For details see the library.%
   13.13  \end{isamarkuptext}%
   13.14 -\end{isabellebody}%
   13.15 +\end{isabelle}%
   13.16  %%% Local Variables:
   13.17  %%% mode: latex
   13.18  %%% TeX-master: "root"
    14.1 --- a/doc-src/TutorialI/Misc/document/Itrev.tex	Tue Aug 29 12:28:48 2000 +0200
    14.2 +++ b/doc-src/TutorialI/Misc/document/Itrev.tex	Tue Aug 29 15:13:10 2000 +0200
    14.3 @@ -1,5 +1,4 @@
    14.4 -%
    14.5 -\begin{isabellebody}%
    14.6 +\begin{isabelle}%
    14.7  %
    14.8  \begin{isamarkuptext}%
    14.9  Function \isa{rev} has quadratic worst-case running time
   14.10 @@ -89,7 +88,7 @@
   14.11  will need to be creative. Additionally, you can read \S\ref{sec:advanced-ind}
   14.12  to learn about some advanced techniques for inductive proofs.%
   14.13  \end{isamarkuptxt}%
   14.14 -\end{isabellebody}%
   14.15 +\end{isabelle}%
   14.16  %%% Local Variables:
   14.17  %%% mode: latex
   14.18  %%% TeX-master: "root"
    15.1 --- a/doc-src/TutorialI/Misc/document/Tree.tex	Tue Aug 29 12:28:48 2000 +0200
    15.2 +++ b/doc-src/TutorialI/Misc/document/Tree.tex	Tue Aug 29 15:13:10 2000 +0200
    15.3 @@ -1,5 +1,4 @@
    15.4 -%
    15.5 -\begin{isabellebody}%
    15.6 +\begin{isabelle}%
    15.7  %
    15.8  \begin{isamarkuptext}%
    15.9  \noindent
   15.10 @@ -17,7 +16,7 @@
   15.11  Define a function \isa{flatten} that flattens a tree into a list
   15.12  by traversing it in infix order. Prove%
   15.13  \end{isamarkuptext}%
   15.14 -\isacommand{lemma}\ {\isachardoublequote}flatten{\isacharparenleft}mirror\ t{\isacharparenright}\ {\isacharequal}\ rev{\isacharparenleft}flatten\ t{\isacharparenright}{\isachardoublequote}\end{isabellebody}%
   15.15 +\isacommand{lemma}\ {\isachardoublequote}flatten{\isacharparenleft}mirror\ t{\isacharparenright}\ {\isacharequal}\ rev{\isacharparenleft}flatten\ t{\isacharparenright}{\isachardoublequote}\end{isabelle}%
   15.16  %%% Local Variables:
   15.17  %%% mode: latex
   15.18  %%% TeX-master: "root"
    16.1 --- a/doc-src/TutorialI/Misc/document/Tree2.tex	Tue Aug 29 12:28:48 2000 +0200
    16.2 +++ b/doc-src/TutorialI/Misc/document/Tree2.tex	Tue Aug 29 15:13:10 2000 +0200
    16.3 @@ -1,5 +1,4 @@
    16.4 -%
    16.5 -\begin{isabellebody}%
    16.6 +\begin{isabelle}%
    16.7  %
    16.8  \begin{isamarkuptext}%
    16.9  \noindent In Exercise~\ref{ex:Tree} we defined a function
   16.10 @@ -12,7 +11,7 @@
   16.11  \begin{isamarkuptext}%
   16.12  \noindent Define \isa{flatten2} and prove%
   16.13  \end{isamarkuptext}%
   16.14 -\isacommand{lemma}\ {\isachardoublequote}flatten\isadigit{2}\ t\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ flatten\ t{\isachardoublequote}\end{isabellebody}%
   16.15 +\isacommand{lemma}\ {\isachardoublequote}flatten\isadigit{2}\ t\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ flatten\ t{\isachardoublequote}\end{isabelle}%
   16.16  %%% Local Variables:
   16.17  %%% mode: latex
   16.18  %%% TeX-master: "root"
    17.1 --- a/doc-src/TutorialI/Misc/document/arith1.tex	Tue Aug 29 12:28:48 2000 +0200
    17.2 +++ b/doc-src/TutorialI/Misc/document/arith1.tex	Tue Aug 29 15:13:10 2000 +0200
    17.3 @@ -1,7 +1,6 @@
    17.4 -%
    17.5 -\begin{isabellebody}%
    17.6 +\begin{isabelle}%
    17.7  \isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ {\isasymnot}\ m\ {\isacharless}\ n{\isacharsemicolon}\ m\ {\isacharless}\ n{\isacharplus}\isadigit{1}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}\isanewline
    17.8 -\end{isabellebody}%
    17.9 +\end{isabelle}%
   17.10  %%% Local Variables:
   17.11  %%% mode: latex
   17.12  %%% TeX-master: "root"
    18.1 --- a/doc-src/TutorialI/Misc/document/arith2.tex	Tue Aug 29 12:28:48 2000 +0200
    18.2 +++ b/doc-src/TutorialI/Misc/document/arith2.tex	Tue Aug 29 15:13:10 2000 +0200
    18.3 @@ -1,8 +1,7 @@
    18.4 -%
    18.5 -\begin{isabellebody}%
    18.6 +\begin{isabelle}%
    18.7  \isacommand{lemma}\ {\isachardoublequote}min\ i\ {\isacharparenleft}max\ j\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ max\ {\isacharparenleft}min\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}\ i{\isacharparenright}\ {\isacharparenleft}min\ i\ {\isacharparenleft}j{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
    18.8  \isacommand{by}{\isacharparenleft}arith{\isacharparenright}\isanewline
    18.9 -\end{isabellebody}%
   18.10 +\end{isabelle}%
   18.11  %%% Local Variables:
   18.12  %%% mode: latex
   18.13  %%% TeX-master: "root"
    19.1 --- a/doc-src/TutorialI/Misc/document/arith3.tex	Tue Aug 29 12:28:48 2000 +0200
    19.2 +++ b/doc-src/TutorialI/Misc/document/arith3.tex	Tue Aug 29 15:13:10 2000 +0200
    19.3 @@ -1,7 +1,6 @@
    19.4 -%
    19.5 -\begin{isabellebody}%
    19.6 +\begin{isabelle}%
    19.7  \isacommand{lemma}\ {\isachardoublequote}n{\isacharasterisk}n\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ n{\isacharequal}\isadigit{0}\ {\isasymor}\ n{\isacharequal}\isadigit{1}{\isachardoublequote}\isanewline
    19.8 -\end{isabellebody}%
    19.9 +\end{isabelle}%
   19.10  %%% Local Variables:
   19.11  %%% mode: latex
   19.12  %%% TeX-master: "root"
    20.1 --- a/doc-src/TutorialI/Misc/document/arith4.tex	Tue Aug 29 12:28:48 2000 +0200
    20.2 +++ b/doc-src/TutorialI/Misc/document/arith4.tex	Tue Aug 29 15:13:10 2000 +0200
    20.3 @@ -1,7 +1,6 @@
    20.4 -%
    20.5 -\begin{isabellebody}%
    20.6 +\begin{isabelle}%
    20.7  \isacommand{lemma}\ {\isachardoublequote}{\isasymnot}\ m\ {\isacharless}\ n\ {\isasymand}\ m\ {\isacharless}\ n{\isacharplus}\isadigit{1}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}\isanewline
    20.8 -\end{isabellebody}%
    20.9 +\end{isabelle}%
   20.10  %%% Local Variables:
   20.11  %%% mode: latex
   20.12  %%% TeX-master: "root"
    21.1 --- a/doc-src/TutorialI/Misc/document/asm_simp.tex	Tue Aug 29 12:28:48 2000 +0200
    21.2 +++ b/doc-src/TutorialI/Misc/document/asm_simp.tex	Tue Aug 29 15:13:10 2000 +0200
    21.3 @@ -1,5 +1,4 @@
    21.4 -%
    21.5 -\begin{isabellebody}%
    21.6 +\begin{isabelle}%
    21.7  %
    21.8  \begin{isamarkuptext}%
    21.9  By default, assumptions are part of the simplification process: they are used
   21.10 @@ -45,7 +44,7 @@
   21.11  Note that only one of the above options is allowed, and it must precede all
   21.12  other arguments.%
   21.13  \end{isamarkuptext}%
   21.14 -\end{isabellebody}%
   21.15 +\end{isabelle}%
   21.16  %%% Local Variables:
   21.17  %%% mode: latex
   21.18  %%% TeX-master: "root"
    22.1 --- a/doc-src/TutorialI/Misc/document/case_splits.tex	Tue Aug 29 12:28:48 2000 +0200
    22.2 +++ b/doc-src/TutorialI/Misc/document/case_splits.tex	Tue Aug 29 15:13:10 2000 +0200
    22.3 @@ -1,5 +1,4 @@
    22.4 -%
    22.5 -\begin{isabellebody}%
    22.6 +\begin{isabelle}%
    22.7  %
    22.8  \begin{isamarkuptext}%
    22.9  Goals containing \isaindex{if}-expressions are usually proved by case
   22.10 @@ -64,8 +63,26 @@
   22.11  \noindent
   22.12  or globally:%
   22.13  \end{isamarkuptext}%
   22.14 -\isacommand{lemmas}\ {\isacharbrackleft}split\ del{\isacharbrackright}\ {\isacharequal}\ list{\isachardot}split\isanewline
   22.15 -\end{isabellebody}%
   22.16 +\isacommand{lemmas}\ {\isacharbrackleft}split\ del{\isacharbrackright}\ {\isacharequal}\ list{\isachardot}split%
   22.17 +\begin{isamarkuptext}%
   22.18 +The above split rules intentionally only affect the conclusion of a
   22.19 +subgoal.  If you want to split an \isa{if} or \isa{case}-expression in
   22.20 +the assumptions, you have to apply \isa{split\_if\_asm} or $t$\isa{.split_asm}:%
   22.21 +\end{isamarkuptext}%
   22.22 +\isacommand{lemma}\ {\isachardoublequote}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ ys\ {\isachartilde}{\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ else\ ys\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}{\isacharequal}{\isachargreater}\ xs\ {\isacharat}\ ys\ {\isachartilde}{\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline
   22.23 +\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ split{\isacharunderscore}if{\isacharunderscore}asm{\isacharparenright}%
   22.24 +\begin{isamarkuptxt}%
   22.25 +\noindent
   22.26 +In contrast to splitting the conclusion, this actually creates two
   22.27 +separate subgoals (which are solved by \isa{simp\_all}):
   22.28 +\begin{isabelle}
   22.29 +\ \isadigit{1}{\isachardot}\ {\isasymlbrakk}\mbox{xs}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ \mbox{ys}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ \mbox{ys}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\isanewline
   22.30 +\ \isadigit{2}{\isachardot}\ {\isasymlbrakk}\mbox{xs}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ \mbox{ys}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ \mbox{xs}\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}
   22.31 +\end{isabelle}
   22.32 +If you need to split both in the assumptions and the conclusion,
   22.33 +use $t$\isa{.splits} which subsumes $t$\isa{.split} and $t$\isa{.split_asm}.%
   22.34 +\end{isamarkuptxt}%
   22.35 +\end{isabelle}%
   22.36  %%% Local Variables:
   22.37  %%% mode: latex
   22.38  %%% TeX-master: "root"
    23.1 --- a/doc-src/TutorialI/Misc/document/cases.tex	Tue Aug 29 12:28:48 2000 +0200
    23.2 +++ b/doc-src/TutorialI/Misc/document/cases.tex	Tue Aug 29 15:13:10 2000 +0200
    23.3 @@ -1,6 +1,17 @@
    23.4 +\begin{isabelle}%
    23.5  %
    23.6 -\begin{isabellebody}%
    23.7 -\isanewline
    23.8 +\isamarkupsubsection{Structural induction and case distinction}
    23.9 +%
   23.10 +\begin{isamarkuptext}%
   23.11 +\indexbold{structural induction}
   23.12 +\indexbold{induction!structural}
   23.13 +\indexbold{case distinction}
   23.14 +Almost all the basic laws about a datatype are applied automatically during
   23.15 +simplification. Only induction is invoked by hand via \isaindex{induct_tac},
   23.16 +which works for any datatype. In some cases, induction is overkill and a case
   23.17 +distinction over all constructors of the datatype suffices. This is performed
   23.18 +by \isaindexbold{case_tac}. A trivial example:%
   23.19 +\end{isamarkuptext}%
   23.20  \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ y{\isacharhash}ys\ {\isasymRightarrow}\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline
   23.21  \isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ xs{\isacharparenright}%
   23.22  \begin{isamarkuptxt}%
   23.23 @@ -12,8 +23,12 @@
   23.24  \end{isabellepar}%
   23.25  which is solved automatically:%
   23.26  \end{isamarkuptxt}%
   23.27 -\isacommand{by}{\isacharparenleft}auto{\isacharparenright}\isanewline
   23.28 -\end{isabellebody}%
   23.29 +\isacommand{by}{\isacharparenleft}auto{\isacharparenright}%
   23.30 +\begin{isamarkuptext}%
   23.31 +Note that we do not need to give a lemma a name if we do not intend to refer
   23.32 +to it explicitly in the future.%
   23.33 +\end{isamarkuptext}%
   23.34 +\end{isabelle}%
   23.35  %%% Local Variables:
   23.36  %%% mode: latex
   23.37  %%% TeX-master: "root"
    24.1 --- a/doc-src/TutorialI/Misc/document/cond_rewr.tex	Tue Aug 29 12:28:48 2000 +0200
    24.2 +++ b/doc-src/TutorialI/Misc/document/cond_rewr.tex	Tue Aug 29 15:13:10 2000 +0200
    24.3 @@ -1,5 +1,4 @@
    24.4 -%
    24.5 -\begin{isabellebody}%
    24.6 +\begin{isabelle}%
    24.7  %
    24.8  \begin{isamarkuptext}%
    24.9  So far all examples of rewrite rules were equations. The simplifier also
   24.10 @@ -24,7 +23,7 @@
   24.11  simplifies to \isa{xs \isasymnoteq\ []}, which is exactly the local
   24.12  assumption of the subgoal.%
   24.13  \end{isamarkuptext}%
   24.14 -\end{isabellebody}%
   24.15 +\end{isabelle}%
   24.16  %%% Local Variables:
   24.17  %%% mode: latex
   24.18  %%% TeX-master: "root"
    25.1 --- a/doc-src/TutorialI/Misc/document/def_rewr.tex	Tue Aug 29 12:28:48 2000 +0200
    25.2 +++ b/doc-src/TutorialI/Misc/document/def_rewr.tex	Tue Aug 29 15:13:10 2000 +0200
    25.3 @@ -1,5 +1,4 @@
    25.4 -%
    25.5 -\begin{isabellebody}%
    25.6 +\begin{isabelle}%
    25.7  %
    25.8  \begin{isamarkuptext}%
    25.9  \noindent Constant definitions (\S\ref{sec:ConstDefinitions}) can
   25.10 @@ -39,7 +38,7 @@
   25.11  You should normally not turn a definition permanently into a simplification
   25.12  rule because this defeats the whole purpose of an abbreviation.%
   25.13  \end{isamarkuptext}%
   25.14 -\end{isabellebody}%
   25.15 +\end{isabelle}%
   25.16  %%% Local Variables:
   25.17  %%% mode: latex
   25.18  %%% TeX-master: "root"
    26.1 --- a/doc-src/TutorialI/Misc/document/fakenat.tex	Tue Aug 29 12:28:48 2000 +0200
    26.2 +++ b/doc-src/TutorialI/Misc/document/fakenat.tex	Tue Aug 29 15:13:10 2000 +0200
    26.3 @@ -1,12 +1,11 @@
    26.4 -%
    26.5 -\begin{isabellebody}%
    26.6 +\begin{isabelle}%
    26.7  %
    26.8  \begin{isamarkuptext}%
    26.9  \noindent
   26.10  The type \isaindexbold{nat}\index{*0|bold}\index{*Suc|bold} of natural
   26.11  numbers is predefined and behaves like%
   26.12  \end{isamarkuptext}%
   26.13 -\isacommand{datatype}\ nat\ {\isacharequal}\ \isadigit{0}\ {\isacharbar}\ Suc\ nat\end{isabellebody}%
   26.14 +\isacommand{datatype}\ nat\ {\isacharequal}\ \isadigit{0}\ {\isacharbar}\ Suc\ nat\end{isabelle}%
   26.15  %%% Local Variables:
   26.16  %%% mode: latex
   26.17  %%% TeX-master: "root"
    27.1 --- a/doc-src/TutorialI/Misc/document/let_rewr.tex	Tue Aug 29 12:28:48 2000 +0200
    27.2 +++ b/doc-src/TutorialI/Misc/document/let_rewr.tex	Tue Aug 29 15:13:10 2000 +0200
    27.3 @@ -1,12 +1,11 @@
    27.4 -%
    27.5 -\begin{isabellebody}%
    27.6 +\begin{isabelle}%
    27.7  \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}let\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ in\ xs{\isacharat}ys{\isacharat}xs{\isacharparenright}\ {\isacharequal}\ ys{\isachardoublequote}\isanewline
    27.8  \isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ Let{\isacharunderscore}def{\isacharparenright}%
    27.9  \begin{isamarkuptext}%
   27.10  If, in a particular context, there is no danger of a combinatorial explosion
   27.11  of nested \isa{let}s one could even add \isa{Let_def} permanently:%
   27.12  \end{isamarkuptext}%
   27.13 -\isacommand{lemmas}\ {\isacharbrackleft}simp{\isacharbrackright}\ {\isacharequal}\ Let{\isacharunderscore}def\end{isabellebody}%
   27.14 +\isacommand{lemmas}\ {\isacharbrackleft}simp{\isacharbrackright}\ {\isacharequal}\ Let{\isacharunderscore}def\end{isabelle}%
   27.15  %%% Local Variables:
   27.16  %%% mode: latex
   27.17  %%% TeX-master: "root"
    28.1 --- a/doc-src/TutorialI/Misc/document/natsum.tex	Tue Aug 29 12:28:48 2000 +0200
    28.2 +++ b/doc-src/TutorialI/Misc/document/natsum.tex	Tue Aug 29 15:13:10 2000 +0200
    28.3 @@ -1,5 +1,4 @@
    28.4 -%
    28.5 -\begin{isabellebody}%
    28.6 +\begin{isabelle}%
    28.7  %
    28.8  \begin{isamarkuptext}%
    28.9  \noindent
   28.10 @@ -23,7 +22,7 @@
   28.11  \isacommand{lemma}\ {\isachardoublequote}sum\ n\ {\isacharplus}\ sum\ n\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequote}\isanewline
   28.12  \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ n{\isacharparenright}\isanewline
   28.13  \isacommand{by}{\isacharparenleft}auto{\isacharparenright}\isanewline
   28.14 -\end{isabellebody}%
   28.15 +\end{isabelle}%
   28.16  %%% Local Variables:
   28.17  %%% mode: latex
   28.18  %%% TeX-master: "root"
    29.1 --- a/doc-src/TutorialI/Misc/document/pairs.tex	Tue Aug 29 12:28:48 2000 +0200
    29.2 +++ b/doc-src/TutorialI/Misc/document/pairs.tex	Tue Aug 29 15:13:10 2000 +0200
    29.3 @@ -1,5 +1,4 @@
    29.4 -%
    29.5 -\begin{isabellebody}%
    29.6 +\begin{isabelle}%
    29.7  %
    29.8  \begin{isamarkuptext}%
    29.9  HOL also has pairs: \isa{($a@1$,$a@2$)} is of type \isa{$\tau@1$ *
   29.10 @@ -21,7 +20,7 @@
   29.11  \end{quote}
   29.12  Further important examples are quantifiers and sets (see~\S\ref{quant-pats}).%
   29.13  \end{isamarkuptext}%
   29.14 -\end{isabellebody}%
   29.15 +\end{isabelle}%
   29.16  %%% Local Variables:
   29.17  %%% mode: latex
   29.18  %%% TeX-master: "root"
    30.1 --- a/doc-src/TutorialI/Misc/document/prime_def.tex	Tue Aug 29 12:28:48 2000 +0200
    30.2 +++ b/doc-src/TutorialI/Misc/document/prime_def.tex	Tue Aug 29 15:13:10 2000 +0200
    30.3 @@ -1,5 +1,4 @@
    30.4 -%
    30.5 -\begin{isabellebody}%
    30.6 +\begin{isabelle}%
    30.7  \isanewline
    30.8  \ \ \ \ {\isachardoublequote}prime{\isacharparenleft}p{\isacharparenright}\ {\isasymequiv}\ \isadigit{1}\ {\isacharless}\ p\ {\isasymand}\ {\isacharparenleft}m\ dvd\ p\ {\isasymlongrightarrow}\ {\isacharparenleft}m{\isacharequal}\isadigit{1}\ {\isasymor}\ m{\isacharequal}p{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
    30.9  \begin{isamarkuptext}%
   30.10 @@ -9,7 +8,7 @@
   30.11  right-hand side, which would introduce an inconsistency (why?). What you
   30.12  should have written is%
   30.13  \end{isamarkuptext}%
   30.14 -\ {\isachardoublequote}prime{\isacharparenleft}p{\isacharparenright}\ {\isasymequiv}\ \isadigit{1}\ {\isacharless}\ p\ {\isasymand}\ {\isacharparenleft}{\isasymforall}m{\isachardot}\ m\ dvd\ p\ {\isasymlongrightarrow}\ {\isacharparenleft}m{\isacharequal}\isadigit{1}\ {\isasymor}\ m{\isacharequal}p{\isacharparenright}{\isacharparenright}{\isachardoublequote}\end{isabellebody}%
   30.15 +\ {\isachardoublequote}prime{\isacharparenleft}p{\isacharparenright}\ {\isasymequiv}\ \isadigit{1}\ {\isacharless}\ p\ {\isasymand}\ {\isacharparenleft}{\isasymforall}m{\isachardot}\ m\ dvd\ p\ {\isasymlongrightarrow}\ {\isacharparenleft}m{\isacharequal}\isadigit{1}\ {\isasymor}\ m{\isacharequal}p{\isacharparenright}{\isacharparenright}{\isachardoublequote}\end{isabelle}%
   30.16  %%% Local Variables:
   30.17  %%% mode: latex
   30.18  %%% TeX-master: "root"
    31.1 --- a/doc-src/TutorialI/Misc/document/trace_simp.tex	Tue Aug 29 12:28:48 2000 +0200
    31.2 +++ b/doc-src/TutorialI/Misc/document/trace_simp.tex	Tue Aug 29 15:13:10 2000 +0200
    31.3 @@ -1,5 +1,4 @@
    31.4 -%
    31.5 -\begin{isabellebody}%
    31.6 +\begin{isabelle}%
    31.7  %
    31.8  \begin{isamarkuptext}%
    31.9  Using the simplifier effectively may take a bit of experimentation.  Set the
   31.10 @@ -37,7 +36,7 @@
   31.11  of rewrite rules). Thus it is advisable to reset it:%
   31.12  \end{isamarkuptxt}%
   31.13  \isacommand{ML}\ {\isachardoublequote}reset\ trace{\isacharunderscore}simp{\isachardoublequote}\isanewline
   31.14 -\end{isabellebody}%
   31.15 +\end{isabelle}%
   31.16  %%% Local Variables:
   31.17  %%% mode: latex
   31.18  %%% TeX-master: "root"
    32.1 --- a/doc-src/TutorialI/Misc/document/types.tex	Tue Aug 29 12:28:48 2000 +0200
    32.2 +++ b/doc-src/TutorialI/Misc/document/types.tex	Tue Aug 29 15:13:10 2000 +0200
    32.3 @@ -1,5 +1,4 @@
    32.4 -%
    32.5 -\begin{isabellebody}%
    32.6 +\begin{isabelle}%
    32.7  \isacommand{types}\ number\ \ \ \ \ \ \ {\isacharequal}\ nat\isanewline
    32.8  \ \ \ \ \ \ gate\ \ \ \ \ \ \ \ \ {\isacharequal}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
    32.9  \ \ \ \ \ \ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}alist\ {\isacharequal}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isacharasterisk}\ {\isacharprime}b{\isacharparenright}list{\isachardoublequote}%
   32.10 @@ -39,7 +38,7 @@
   32.11  in which case the default name of each definition is \isa{$f$_def}, where
   32.12  $f$ is the name of the defined constant.%
   32.13  \end{isamarkuptext}%
   32.14 -\end{isabellebody}%
   32.15 +\end{isabelle}%
   32.16  %%% Local Variables:
   32.17  %%% mode: latex
   32.18  %%% TeX-master: "root"
    33.1 --- a/doc-src/TutorialI/Recdef/Nested2.thy	Tue Aug 29 12:28:48 2000 +0200
    33.2 +++ b/doc-src/TutorialI/Recdef/Nested2.thy	Tue Aug 29 15:13:10 2000 +0200
    33.3 @@ -34,10 +34,21 @@
    33.4  both of which are solved by simplification:
    33.5  *};
    33.6  
    33.7 -by(simp_all del:map_compose add:sym[OF map_compose] rev_map);
    33.8 +by(simp_all add:rev_map sym[OF map_compose]);
    33.9  
   33.10  text{*\noindent
   33.11 -If this surprises you, see Datatype/Nested2......
   33.12 +If the proof of the induction step mystifies you, we recommend to go through
   33.13 +the chain of simplification steps in detail, probably with the help of
   33.14 +\isa{trace\_simp}.
   33.15 +%\begin{quote}
   33.16 +%{term[display]"trev(trev(App f ts))"}\\
   33.17 +%{term[display]"App f (rev(map trev (rev(map trev ts))))"}\\
   33.18 +%{term[display]"App f (map trev (rev(rev(map trev ts))))"}\\
   33.19 +%{term[display]"App f (map trev (map trev ts))"}\\
   33.20 +%{term[display]"App f (map (trev o trev) ts)"}\\
   33.21 +%{term[display]"App f (map (%x. x) ts)"}\\
   33.22 +%{term[display]"App f ts"}
   33.23 +%\end{quote}
   33.24  
   33.25  The above definition of @{term"trev"} is superior to the one in \S\ref{sec:nested-datatype}
   33.26  because it brings @{term"rev"} into play, about which already know a lot, in particular
   33.27 @@ -48,19 +59,22 @@
   33.28  because they determine the complexity of your proofs.}
   33.29  \end{quote}
   33.30  
   33.31 -Let us now return to the question of how \isacommand{recdef} can come up with sensible termination
   33.32 -conditions in the presence of higher-order functions like @{term"map"}. For a start, if nothing
   33.33 -were known about @{term"map"}, @{term"map trev ts"} might apply @{term"trev"} to arbitrary terms,
   33.34 -and thus \isacommand{recdef} would try to prove the unprovable
   33.35 -@{term"size t < Suc (term_size ts)"}, without any assumption about \isa{t}.
   33.36 -Therefore \isacommand{recdef} has been supplied with the congruence theorem \isa{map\_cong}: 
   33.37 +Let us now return to the question of how \isacommand{recdef} can come up with
   33.38 +sensible termination conditions in the presence of higher-order functions
   33.39 +like @{term"map"}. For a start, if nothing were known about @{term"map"},
   33.40 +@{term"map trev ts"} might apply @{term"trev"} to arbitrary terms, and thus
   33.41 +\isacommand{recdef} would try to prove the unprovable @{term"size t < Suc
   33.42 +(term_size ts)"}, without any assumption about \isa{t}.  Therefore
   33.43 +\isacommand{recdef} has been supplied with the congruence theorem
   33.44 +\isa{map\_cong}:
   33.45  \begin{quote}
   33.46  @{thm[display,margin=50]"map_cong"[no_vars]}
   33.47  \end{quote}
   33.48 -Its second premise expresses (indirectly) that the second argument of @{term"map"} is only applied
   33.49 -to elements of its third argument. Congruence rules for other higher-order functions on lists would
   33.50 -look very similar but have not been proved yet because they were never needed.
   33.51 -If you get into a situation where you need to supply \isacommand{recdef} with new congruence
   33.52 +Its second premise expresses (indirectly) that the second argument of
   33.53 +@{term"map"} is only applied to elements of its third argument. Congruence
   33.54 +rules for other higher-order functions on lists would look very similar but
   33.55 +have not been proved yet because they were never needed. If you get into a
   33.56 +situation where you need to supply \isacommand{recdef} with new congruence
   33.57  rules, you can either append the line
   33.58  \begin{ttbox}
   33.59  congs <congruence rules>
    34.1 --- a/doc-src/TutorialI/Recdef/document/Induction.tex	Tue Aug 29 12:28:48 2000 +0200
    34.2 +++ b/doc-src/TutorialI/Recdef/document/Induction.tex	Tue Aug 29 15:13:10 2000 +0200
    34.3 @@ -1,5 +1,4 @@
    34.4 -%
    34.5 -\begin{isabellebody}%
    34.6 +\begin{isabelle}%
    34.7  %
    34.8  \begin{isamarkuptext}%
    34.9  Assuming we have defined our function such that Isabelle could prove
   34.10 @@ -63,7 +62,7 @@
   34.11  empty list, the singleton list, and the list with at least two elements
   34.12  (in which case you may assume it holds for the tail of that list).%
   34.13  \end{isamarkuptext}%
   34.14 -\end{isabellebody}%
   34.15 +\end{isabelle}%
   34.16  %%% Local Variables:
   34.17  %%% mode: latex
   34.18  %%% TeX-master: "root"
    35.1 --- a/doc-src/TutorialI/Recdef/document/Nested0.tex	Tue Aug 29 12:28:48 2000 +0200
    35.2 +++ b/doc-src/TutorialI/Recdef/document/Nested0.tex	Tue Aug 29 15:13:10 2000 +0200
    35.3 @@ -1,5 +1,4 @@
    35.4 -%
    35.5 -\begin{isabellebody}%
    35.6 +\begin{isabelle}%
    35.7  %
    35.8  \begin{isamarkuptext}%
    35.9  In \S\ref{sec:nested-datatype} we defined the datatype of terms%
   35.10 @@ -17,7 +16,7 @@
   35.11  
   35.12  FIXME: declare trev now!%
   35.13  \end{isamarkuptext}%
   35.14 -\end{isabellebody}%
   35.15 +\end{isabelle}%
   35.16  %%% Local Variables:
   35.17  %%% mode: latex
   35.18  %%% TeX-master: "root"
    36.1 --- a/doc-src/TutorialI/Recdef/document/Nested1.tex	Tue Aug 29 12:28:48 2000 +0200
    36.2 +++ b/doc-src/TutorialI/Recdef/document/Nested1.tex	Tue Aug 29 15:13:10 2000 +0200
    36.3 @@ -1,5 +1,4 @@
    36.4 -%
    36.5 -\begin{isabellebody}%
    36.6 +\begin{isabelle}%
    36.7  \isacommand{consts}\ trev\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ {\isacharequal}{\isachargreater}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isachardoublequote}%
    36.8  \begin{isamarkuptext}%
    36.9  \noindent
   36.10 @@ -39,7 +38,7 @@
   36.11  We will now prove the termination condition and continue with our definition.
   36.12  Below we return to the question of how \isacommand{recdef} ``knows'' about \isa{map}.%
   36.13  \end{isamarkuptext}%
   36.14 -\end{isabellebody}%
   36.15 +\end{isabelle}%
   36.16  %%% Local Variables:
   36.17  %%% mode: latex
   36.18  %%% TeX-master: "root"
    37.1 --- a/doc-src/TutorialI/Recdef/document/Nested2.tex	Tue Aug 29 12:28:48 2000 +0200
    37.2 +++ b/doc-src/TutorialI/Recdef/document/Nested2.tex	Tue Aug 29 15:13:10 2000 +0200
    37.3 @@ -1,5 +1,4 @@
    37.4 -%
    37.5 -\begin{isabellebody}%
    37.6 +\begin{isabelle}%
    37.7  %
    37.8  \begin{isamarkuptext}%
    37.9  \noindent
   37.10 @@ -32,10 +31,21 @@
   37.11  \end{quote}
   37.12  both of which are solved by simplification:%
   37.13  \end{isamarkuptxt}%
   37.14 -\isacommand{by}{\isacharparenleft}simp{\isacharunderscore}all\ del{\isacharcolon}map{\isacharunderscore}compose\ add{\isacharcolon}sym{\isacharbrackleft}OF\ map{\isacharunderscore}compose{\isacharbrackright}\ rev{\isacharunderscore}map{\isacharparenright}%
   37.15 +\isacommand{by}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}rev{\isacharunderscore}map\ sym{\isacharbrackleft}OF\ map{\isacharunderscore}compose{\isacharbrackright}{\isacharparenright}%
   37.16  \begin{isamarkuptext}%
   37.17  \noindent
   37.18 -If this surprises you, see Datatype/Nested2......
   37.19 +If the proof of the induction step mystifies you, we recommend to go through
   37.20 +the chain of simplification steps in detail, probably with the help of
   37.21 +\isa{trace\_simp}.
   37.22 +%\begin{quote}
   37.23 +%{term[display]"trev(trev(App f ts))"}\\
   37.24 +%{term[display]"App f (rev(map trev (rev(map trev ts))))"}\\
   37.25 +%{term[display]"App f (map trev (rev(rev(map trev ts))))"}\\
   37.26 +%{term[display]"App f (map trev (map trev ts))"}\\
   37.27 +%{term[display]"App f (map (trev o trev) ts)"}\\
   37.28 +%{term[display]"App f (map (%x. x) ts)"}\\
   37.29 +%{term[display]"App f ts"}
   37.30 +%\end{quote}
   37.31  
   37.32  The above definition of \isa{trev} is superior to the one in \S\ref{sec:nested-datatype}
   37.33  because it brings \isa{rev} into play, about which already know a lot, in particular
   37.34 @@ -46,12 +56,13 @@
   37.35  because they determine the complexity of your proofs.}
   37.36  \end{quote}
   37.37  
   37.38 -Let us now return to the question of how \isacommand{recdef} can come up with sensible termination
   37.39 -conditions in the presence of higher-order functions like \isa{map}. For a start, if nothing
   37.40 -were known about \isa{map}, \isa{map\ trev\ \mbox{ts}} might apply \isa{trev} to arbitrary terms,
   37.41 -and thus \isacommand{recdef} would try to prove the unprovable
   37.42 -\isa{size\ \mbox{t}\ {\isacharless}\ Suc\ {\isacharparenleft}term{\isacharunderscore}size\ \mbox{ts}{\isacharparenright}}, without any assumption about \isa{t}.
   37.43 -Therefore \isacommand{recdef} has been supplied with the congruence theorem \isa{map\_cong}: 
   37.44 +Let us now return to the question of how \isacommand{recdef} can come up with
   37.45 +sensible termination conditions in the presence of higher-order functions
   37.46 +like \isa{map}. For a start, if nothing were known about \isa{map},
   37.47 +\isa{map\ trev\ \mbox{ts}} might apply \isa{trev} to arbitrary terms, and thus
   37.48 +\isacommand{recdef} would try to prove the unprovable \isa{size\ \mbox{t}\ {\isacharless}\ Suc\ {\isacharparenleft}term{\isacharunderscore}size\ \mbox{ts}{\isacharparenright}}, without any assumption about \isa{t}.  Therefore
   37.49 +\isacommand{recdef} has been supplied with the congruence theorem
   37.50 +\isa{map\_cong}:
   37.51  \begin{quote}
   37.52  
   37.53  \begin{isabelle}%
   37.54 @@ -60,10 +71,11 @@
   37.55  \end{isabelle}%
   37.56  
   37.57  \end{quote}
   37.58 -Its second premise expresses (indirectly) that the second argument of \isa{map} is only applied
   37.59 -to elements of its third argument. Congruence rules for other higher-order functions on lists would
   37.60 -look very similar but have not been proved yet because they were never needed.
   37.61 -If you get into a situation where you need to supply \isacommand{recdef} with new congruence
   37.62 +Its second premise expresses (indirectly) that the second argument of
   37.63 +\isa{map} is only applied to elements of its third argument. Congruence
   37.64 +rules for other higher-order functions on lists would look very similar but
   37.65 +have not been proved yet because they were never needed. If you get into a
   37.66 +situation where you need to supply \isacommand{recdef} with new congruence
   37.67  rules, you can either append the line
   37.68  \begin{ttbox}
   37.69  congs <congruence rules>
   37.70 @@ -78,7 +90,7 @@
   37.71  declaring a congruence rule for the simplifier does not make it
   37.72  available to \isacommand{recdef}, and vice versa. This is intentional.%
   37.73  \end{isamarkuptext}%
   37.74 -\end{isabellebody}%
   37.75 +\end{isabelle}%
   37.76  %%% Local Variables:
   37.77  %%% mode: latex
   37.78  %%% TeX-master: "root"
    38.1 --- a/doc-src/TutorialI/Recdef/document/examples.tex	Tue Aug 29 12:28:48 2000 +0200
    38.2 +++ b/doc-src/TutorialI/Recdef/document/examples.tex	Tue Aug 29 15:13:10 2000 +0200
    38.3 @@ -1,5 +1,4 @@
    38.4 -%
    38.5 -\begin{isabellebody}%
    38.6 +\begin{isabelle}%
    38.7  %
    38.8  \begin{isamarkuptext}%
    38.9  Here is a simple example, the Fibonacci function:%
   38.10 @@ -78,7 +77,7 @@
   38.11  For non-recursive functions the termination measure degenerates to the empty
   38.12  set \isa{\{\}}.%
   38.13  \end{isamarkuptext}%
   38.14 -\end{isabellebody}%
   38.15 +\end{isabelle}%
   38.16  %%% Local Variables:
   38.17  %%% mode: latex
   38.18  %%% TeX-master: "root"
    39.1 --- a/doc-src/TutorialI/Recdef/document/simplification.tex	Tue Aug 29 12:28:48 2000 +0200
    39.2 +++ b/doc-src/TutorialI/Recdef/document/simplification.tex	Tue Aug 29 15:13:10 2000 +0200
    39.3 @@ -1,5 +1,4 @@
    39.4 -%
    39.5 -\begin{isabellebody}%
    39.6 +\begin{isabelle}%
    39.7  %
    39.8  \begin{isamarkuptext}%
    39.9  Once we have succeeded in proving all termination conditions, the recursion
   39.10 @@ -101,7 +100,7 @@
   39.11  after which we can disable the original simplification rule:%
   39.12  \end{isamarkuptext}%
   39.13  \isacommand{lemmas}\ {\isacharbrackleft}simp\ del{\isacharbrackright}\ {\isacharequal}\ gcd{\isachardot}simps\isanewline
   39.14 -\end{isabellebody}%
   39.15 +\end{isabelle}%
   39.16  %%% Local Variables:
   39.17  %%% mode: latex
   39.18  %%% TeX-master: "root"
    40.1 --- a/doc-src/TutorialI/Recdef/document/termination.tex	Tue Aug 29 12:28:48 2000 +0200
    40.2 +++ b/doc-src/TutorialI/Recdef/document/termination.tex	Tue Aug 29 15:13:10 2000 +0200
    40.3 @@ -1,5 +1,4 @@
    40.4 -%
    40.5 -\begin{isabellebody}%
    40.6 +\begin{isabelle}%
    40.7  %
    40.8  \begin{isamarkuptext}%
    40.9  When a function is defined via \isacommand{recdef}, Isabelle tries to prove
   40.10 @@ -87,7 +86,7 @@
   40.11  For details see the manual~\cite{isabelle-HOL} and the examples in the
   40.12  library.%
   40.13  \end{isamarkuptext}%
   40.14 -\end{isabellebody}%
   40.15 +\end{isabelle}%
   40.16  %%% Local Variables:
   40.17  %%% mode: latex
   40.18  %%% TeX-master: "root"
    41.1 --- a/doc-src/TutorialI/ToyList/document/ToyList.tex	Tue Aug 29 12:28:48 2000 +0200
    41.2 +++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Tue Aug 29 15:13:10 2000 +0200
    41.3 @@ -1,5 +1,4 @@
    41.4 -%
    41.5 -\begin{isabellebody}%
    41.6 +\begin{isabelle}%
    41.7  \isacommand{theory}\ ToyList\ {\isacharequal}\ PreList{\isacharcolon}%
    41.8  \begin{isamarkuptext}%
    41.9  \noindent
   41.10 @@ -325,7 +324,7 @@
   41.11  we are finished with its development:%
   41.12  \end{isamarkuptext}%
   41.13  \isacommand{end}\isanewline
   41.14 -\end{isabellebody}%
   41.15 +\end{isabelle}%
   41.16  %%% Local Variables:
   41.17  %%% mode: latex
   41.18  %%% TeX-master: "root"
    42.1 --- a/doc-src/TutorialI/Trie/document/Option2.tex	Tue Aug 29 12:28:48 2000 +0200
    42.2 +++ b/doc-src/TutorialI/Trie/document/Option2.tex	Tue Aug 29 15:13:10 2000 +0200
    42.3 @@ -1,7 +1,6 @@
    42.4 -%
    42.5 -\begin{isabellebody}%
    42.6 +\begin{isabelle}%
    42.7  \isanewline
    42.8 -\isacommand{datatype}\ {\isacharprime}a\ option\ {\isacharequal}\ None\ {\isacharbar}\ Some\ {\isacharprime}a\end{isabellebody}%
    42.9 +\isacommand{datatype}\ {\isacharprime}a\ option\ {\isacharequal}\ None\ {\isacharbar}\ Some\ {\isacharprime}a\end{isabelle}%
   42.10  %%% Local Variables:
   42.11  %%% mode: latex
   42.12  %%% TeX-master: "root"
    43.1 --- a/doc-src/TutorialI/Trie/document/Trie.tex	Tue Aug 29 12:28:48 2000 +0200
    43.2 +++ b/doc-src/TutorialI/Trie/document/Trie.tex	Tue Aug 29 15:13:10 2000 +0200
    43.3 @@ -1,5 +1,4 @@
    43.4 -%
    43.5 -\begin{isabellebody}%
    43.6 +\begin{isabelle}%
    43.7  %
    43.8  \begin{isamarkuptext}%
    43.9  To minimize running time, each node of a trie should contain an array that maps
   43.10 @@ -123,7 +122,7 @@
   43.11  solves the proof. Part~\ref{Isar} shows you how to write readable and stable
   43.12  proofs.%
   43.13  \end{isamarkuptext}%
   43.14 -\end{isabellebody}%
   43.15 +\end{isabelle}%
   43.16  %%% Local Variables:
   43.17  %%% mode: latex
   43.18  %%% TeX-master: "root"
    44.1 --- a/doc-src/TutorialI/fp.tex	Tue Aug 29 12:28:48 2000 +0200
    44.2 +++ b/doc-src/TutorialI/fp.tex	Tue Aug 29 15:13:10 2000 +0200
    44.3 @@ -214,66 +214,7 @@
    44.4  \input{Misc/document/Tree.tex}%
    44.5  \end{exercise}
    44.6  
    44.7 -\subsection{Case expressions}
    44.8 -\label{sec:case-expressions}
    44.9 -
   44.10 -HOL also features \isaindexbold{case}-expressions for analyzing
   44.11 -elements of a datatype. For example,
   44.12 -% case xs of [] => 0 | y#ys => y
   44.13 -\begin{isabellepar}%
   44.14 -~~~case~xs~of~[]~{\isasymRightarrow}~0~|~y~\#~ys~{\isasymRightarrow}~y
   44.15 -\end{isabellepar}%
   44.16 -evaluates to \isa{0} if \isa{xs} is \isa{[]} and to \isa{y} if 
   44.17 -\isa{xs} is \isa{y\#ys}. (Since the result in both branches must be of
   44.18 -the same type, it follows that \isa{y::nat} and hence
   44.19 -\isa{xs::(nat)list}.)
   44.20 -
   44.21 -In general, if $e$ is a term of the datatype $t$ defined in
   44.22 -\S\ref{sec:general-datatype} above, the corresponding
   44.23 -\isa{case}-expression analyzing $e$ is
   44.24 -\[
   44.25 -\begin{array}{rrcl}
   44.26 -\isa{case}~e~\isa{of} & C@1~x@{11}~\dots~x@{1k@1} & \To & e@1 \\
   44.27 -                           \vdots \\
   44.28 -                           \mid & C@m~x@{m1}~\dots~x@{mk@m} & \To & e@m
   44.29 -\end{array}
   44.30 -\]
   44.31 -
   44.32 -\begin{warn}
   44.33 -{\em All} constructors must be present, their order is fixed, and nested
   44.34 -patterns are not supported.  Violating these restrictions results in strange
   44.35 -error messages.
   44.36 -\end{warn}
   44.37 -\noindent
   44.38 -Nested patterns can be simulated by nested \isa{case}-expressions: instead
   44.39 -of
   44.40 -% case xs of [] => 0 | [x] => x | x#(y#zs) => y
   44.41 -\begin{isabellepar}%
   44.42 -~~~case~xs~of~[]~{\isasymRightarrow}~0~|~[x]~{\isasymRightarrow}~x~|~x~\#~y~\#~zs~{\isasymRightarrow}~y
   44.43 -\end{isabellepar}%
   44.44 -write
   44.45 -% term(latex xsymbols symbols)"case xs of [] => 0 | x#ys => (case ys of [] => x | y#zs => y)";
   44.46 -\begin{isabellepar}%
   44.47 -~~~case~xs~of~[]~{\isasymRightarrow}~0~|~x~\#~ys~{\isasymRightarrow}~(case~ys~of~[]~{\isasymRightarrow}~x~|~y~\#~zs~{\isasymRightarrow}~y)%
   44.48 -\end{isabellepar}%
   44.49 -Note that \isa{case}-expressions should be enclosed in parentheses to
   44.50 -indicate their scope.
   44.51 -
   44.52 -\subsection{Structural induction and case distinction}
   44.53 -\indexbold{structural induction}
   44.54 -\indexbold{induction!structural}
   44.55 -\indexbold{case distinction}
   44.56 -
   44.57 -Almost all the basic laws about a datatype are applied automatically during
   44.58 -simplification. Only induction is invoked by hand via \isaindex{induct_tac},
   44.59 -which works for any datatype. In some cases, induction is overkill and a case
   44.60 -distinction over all constructors of the datatype suffices. This is performed
   44.61 -by \isaindexbold{case_tac}. A trivial example:
   44.62 -
   44.63 -\input{Misc/document/cases.tex}%
   44.64 -
   44.65 -Note that we do not need to give a lemma a name if we do not intend to refer
   44.66 -to it explicitly in the future.
   44.67 +\input{Misc/document/case_exprs.tex}
   44.68  
   44.69  \begin{warn}
   44.70    Induction is only allowed on free (or \isasymAnd-bound) variables that
   44.71 @@ -592,7 +533,6 @@
   44.72  \index{*split|(}
   44.73  
   44.74  {\makeatother\input{Misc/document/case_splits.tex}}
   44.75 -
   44.76  \index{*split|)}
   44.77  
   44.78  \begin{warn}
   44.79 @@ -620,10 +560,10 @@
   44.80  
   44.81  \subsubsection{Permutative rewrite rules}
   44.82  
   44.83 -A rewrite rule is {\bf permutative} if the left-hand side and right-hand side
   44.84 -are the same up to renaming of variables.  The most common permutative rule
   44.85 -is commutativity: $x+y = y+x$.  Another example is $(x-y)-z = (x-z)-y$.  Such
   44.86 -rules are problematic because once they apply, they can be used forever.
   44.87 +A rewrite rule is \textbf{permutative} if the left-hand side and right-hand
   44.88 +side are the same up to renaming of variables.  The most common permutative
   44.89 +rule is commutativity: $x+y = y+x$.  Another example is $(x-y)-z = (x-z)-y$.
   44.90 +Such rules are problematic because once they apply, they can be used forever.
   44.91  The simplifier is aware of this danger and treats permutative rules
   44.92  separately. For details see~\cite{isabelle-ref}.
   44.93  
    45.1 --- a/src/Provers/classical.ML	Tue Aug 29 12:28:48 2000 +0200
    45.2 +++ b/src/Provers/classical.ML	Tue Aug 29 15:13:10 2000 +0200
    45.3 @@ -683,15 +683,13 @@
    45.4  
    45.5  (*Add/replace a safe wrapper*)
    45.6  fun cs addSWrapper new_swrapper = update_swrappers cs (fn swrappers =>
    45.7 -    (case assoc_string (swrappers,(fst new_swrapper)) of None =>()
    45.8 -	   | Some x => warning("overwriting safe wrapper "^fst new_swrapper); 
    45.9 -		   overwrite (swrappers, new_swrapper)));
   45.10 +    overwrite_warn (swrappers, new_swrapper)
   45.11 +       ("Overwriting safe wrapper " ^ fst new_swrapper));
   45.12  
   45.13  (*Add/replace an unsafe wrapper*)
   45.14  fun cs addWrapper new_uwrapper = update_uwrappers cs (fn uwrappers =>
   45.15 -    (case assoc_string (uwrappers,(fst new_uwrapper)) of None =>()
   45.16 -	   | Some x => warning ("overwriting unsafe wrapper "^fst new_uwrapper);
   45.17 -		   overwrite (uwrappers, new_uwrapper)));
   45.18 +    overwrite_warn (uwrappers, new_uwrapper)
   45.19 +	("Overwriting unsafe wrapper "^fst new_uwrapper));
   45.20  
   45.21  (*Remove a safe wrapper*)
   45.22  fun cs delSWrapper name = update_swrappers cs (fn swrappers =>
    46.1 --- a/src/Pure/library.ML	Tue Aug 29 12:28:48 2000 +0200
    46.2 +++ b/src/Pure/library.ML	Tue Aug 29 15:13:10 2000 +0200
    46.3 @@ -188,6 +188,7 @@
    46.4    val assoc2: (''a * (''b * 'c) list) list * (''a * ''b) -> 'c option
    46.5    val gen_assoc: ('a * 'b -> bool) -> ('b * 'c) list * 'a -> 'c option
    46.6    val overwrite: (''a * 'b) list * (''a * 'b) -> (''a * 'b) list
    46.7 +  val overwrite_warn: (''a * 'b) list * (''a * 'b) -> string -> (''a * 'b) list
    46.8    val gen_overwrite: ('a * 'a -> bool) -> ('a * 'b) list * ('a * 'b) -> ('a * 'b) list
    46.9  
   46.10    (*generic tables*)
   46.11 @@ -1204,6 +1205,10 @@
   46.12  
   46.13  (** misc **)
   46.14  
   46.15 +fun overwrite_warn (args as (alist,(a,_))) text =
   46.16 +  (if is_none(assoc(alist,a)) then () else warning text;
   46.17 +   overwrite args);
   46.18 +
   46.19  (*use the keyfun to make a list of (x, key) pairs*)
   46.20  fun make_keylist (keyfun: 'a->'b) : 'a list -> ('a * 'b) list =
   46.21    let fun keypair x = (x, keyfun x)
    47.1 --- a/src/Pure/term.ML	Tue Aug 29 12:28:48 2000 +0200
    47.2 +++ b/src/Pure/term.ML	Tue Aug 29 15:13:10 2000 +0200
    47.3 @@ -638,16 +638,14 @@
    47.4    | subst_atomic (instl: (term*term) list) t =
    47.5        let fun subst (Abs(a,T,body)) = Abs(a, T, subst body)
    47.6              | subst (f$t') = subst f $ subst t'
    47.7 -            | subst t = (case assoc(instl,t) of
    47.8 -                           Some u => u  |  None => t)
    47.9 +            | subst t = if_none (assoc(instl,t)) t
   47.10        in  subst t  end;
   47.11  
   47.12  (*Substitute for type Vars in a type*)
   47.13  fun typ_subst_TVars iTs T = if null iTs then T else
   47.14    let fun subst(Type(a,Ts)) = Type(a, map subst Ts)
   47.15          | subst(T as TFree _) = T
   47.16 -        | subst(T as TVar(ixn,_)) =
   47.17 -            (case assoc(iTs,ixn) of None => T | Some(U) => U)
   47.18 +        | subst(T as TVar(ixn,_)) = if_none (assoc(iTs,ixn)) T
   47.19    in subst T end;
   47.20  
   47.21  (*Substitute for type Vars in a term*)
   47.22 @@ -655,8 +653,7 @@
   47.23  
   47.24  (*Substitute for Vars in a term; see also envir/norm_term*)
   47.25  fun subst_Vars itms t = if null itms then t else
   47.26 -  let fun subst(v as Var(ixn,_)) =
   47.27 -            (case assoc(itms,ixn) of None => v | Some t => t)
   47.28 +  let fun subst(v as Var(ixn,_)) = if_none (assoc(itms,ixn)) v
   47.29          | subst(Abs(a,T,t)) = Abs(a,T,subst t)
   47.30          | subst(f$t) = subst f $ subst t
   47.31          | subst(t) = t
    48.1 --- a/src/Pure/thm.ML	Tue Aug 29 12:28:48 2000 +0200
    48.2 +++ b/src/Pure/thm.ML	Tue Aug 29 15:13:10 2000 +0200
    48.3 @@ -1363,8 +1363,7 @@
    48.4                                else Var((y,i),T)
    48.5                   | None=> t)
    48.6            | rename(Abs(x,T,t)) =
    48.7 -              Abs(case assoc_string(al,x) of Some(y) => y | None => x,
    48.8 -                  T, rename t)
    48.9 +              Abs(if_none(assoc_string(al,x)) x, T, rename t)
   48.10            | rename(f$t) = rename f $ rename t
   48.11            | rename(t) = t;
   48.12          fun strip_ren Ai = strip_apply rename (Ai,B)
   48.13 @@ -1835,10 +1834,11 @@
   48.14      val (a, _) = dest_Const (head_of lhs) handle TERM _ =>
   48.15        raise SIMPLIFIER ("Congruence must start with a constant", thm);
   48.16      val (alist,weak) = congs
   48.17 +    val alist2 = overwrite_warn (alist, (a,{lhs=lhs, thm=thm}))
   48.18 +           ("Overwriting congruence rule for " ^ quote a);
   48.19      val weak2 = if is_full_cong thm then weak else a::weak
   48.20    in
   48.21 -    mk_mss (rules, ((a, {lhs = lhs, thm = thm}) :: alist, weak2),
   48.22 -            procs, bounds, prems, mk_rews, termless)
   48.23 +    mk_mss (rules, (alist2,weak2), procs, bounds, prems, mk_rews, termless)
   48.24    end;
   48.25  
   48.26  val (op add_congs) = foldl add_cong;
   48.27 @@ -1969,7 +1969,7 @@
   48.28  fun ren_inst(insts,prop,pat,obj) =
   48.29    let val ren = match_bvs(pat,obj,[])
   48.30        fun renAbs(Abs(x,T,b)) =
   48.31 -            Abs(case assoc_string(ren,x) of None => x | Some(y) => y, T, renAbs(b))
   48.32 +            Abs(if_none(assoc_string(ren,x)) x, T, renAbs(b))
   48.33          | renAbs(f$t) = renAbs(f) $ renAbs(t)
   48.34          | renAbs(t) = t
   48.35    in subst_vars insts (if null(ren) then prop else renAbs(prop)) end;