--- a/doc-src/TutorialI/Inductive/AB.thy Tue Jun 28 12:32:38 2005 +0200
+++ b/doc-src/TutorialI/Inductive/AB.thy Tue Jun 28 15:26:32 2005 +0200
@@ -133,8 +133,8 @@
*}
apply(induct_tac w)
- apply(simp)
-by(force simp add: zabs_def take_Cons split: nat.split if_splits)
+apply(auto simp add: abs_if take_Cons split: nat.split)
+done
text{*
Finally we come to the above-mentioned lemma about cutting in half a word with two more elements of one sort than of the other sort:
--- a/doc-src/TutorialI/Inductive/document/AB.tex Tue Jun 28 12:32:38 2005 +0200
+++ b/doc-src/TutorialI/Inductive/document/AB.tex Tue Jun 28 15:26:32 2005 +0200
@@ -145,10 +145,10 @@
\end{isamarkuptxt}%
\isamarkuptrue%
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ w{\isacharparenright}\isanewline
-\ \isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
\isamarkupfalse%
-\isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}\ zabs{\isacharunderscore}def\ take{\isacharunderscore}Cons\ split{\isacharcolon}\ nat{\isachardot}split\ if{\isacharunderscore}splits{\isacharparenright}\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ abs{\isacharunderscore}if\ take{\isacharunderscore}Cons\ split{\isacharcolon}\ nat{\isachardot}split{\isacharparenright}\isanewline
+\isamarkupfalse%
+\isacommand{done}\isamarkupfalse%
%
\begin{isamarkuptext}%
Finally we come to the above-mentioned lemma about cutting in half a word with two more elements of one sort than of the other sort:%
--- a/doc-src/TutorialI/Types/Numbers.thy Tue Jun 28 12:32:38 2005 +0200
+++ b/doc-src/TutorialI/Types/Numbers.thy Tue Jun 28 15:26:32 2005 +0200
@@ -166,7 +166,7 @@
by arith
lemma "abs (2*x) = 2 * abs (x :: int)"
-by (simp add: zabs_def)
+by (simp add: abs_if)
text {*Induction rules for the Integers
--- a/doc-src/TutorialI/Types/document/Numbers.tex Tue Jun 28 12:32:38 2005 +0200
+++ b/doc-src/TutorialI/Types/document/Numbers.tex Tue Jun 28 15:26:32 2005 +0200
@@ -269,7 +269,7 @@
\isamarkupfalse%
\isacommand{lemma}\ {\isachardoublequote}abs\ {\isacharparenleft}{\isadigit{2}}{\isacharasterisk}x{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ abs\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ int{\isacharparenright}{\isachardoublequote}\isanewline
\isamarkupfalse%
-\isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ zabs{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
+\isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ abs{\isacharunderscore}if{\isacharparenright}\isamarkupfalse%
%
\begin{isamarkuptext}%
Induction rules for the Integers
--- a/doc-src/TutorialI/isabelle.sty Tue Jun 28 12:32:38 2005 +0200
+++ b/doc-src/TutorialI/isabelle.sty Tue Jun 28 15:26:32 2005 +0200
@@ -22,10 +22,10 @@
\newcommand{\isamath}[1]{\emph{$#1$}}
\newcommand{\isatext}[1]{\emph{#1}}
\newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
-\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
-\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
-\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
-\newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
+\newcommand{\isactrlsub}[1]{\emph{${}\sb{\mbox{\isastylescript{#1}}}$}}
+\newcommand{\isactrlsup}[1]{\emph{${}\sp{\mbox{\isastylescript{#1}}}$}}
+\newcommand{\isactrlisub}[1]{\emph{${}\sb{\mbox{\isastylescript{#1}}}$}}
+\newcommand{\isactrlisup}[1]{\emph{${}\sp{\mbox{\isastylescript{#1}}}$}}
\newcommand{\isactrlbsub}{\emph\bgroup\begin{math}{}\sb\bgroup\mbox\bgroup\isastylescript}
\newcommand{\isactrlesub}{\egroup\egroup\end{math}\egroup}
\newcommand{\isactrlbsup}{\emph\bgroup\begin{math}{}\sp\bgroup\mbox\bgroup\isastylescript}