# HG changeset patch
# User paulson
# Date 1119965192 -7200
# Node ID 02cf78f0afce33e0081fc7ee05d853b8d3a7df40
# Parent  991ecdd985d932530896d7882c46655c12443606
replacing zabs_def by abs_if

diff -r 991ecdd985d9 -r 02cf78f0afce doc-src/TutorialI/Inductive/AB.thy
--- 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:
diff -r 991ecdd985d9 -r 02cf78f0afce doc-src/TutorialI/Inductive/document/AB.tex
--- 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:%
diff -r 991ecdd985d9 -r 02cf78f0afce doc-src/TutorialI/Types/Numbers.thy
--- 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
diff -r 991ecdd985d9 -r 02cf78f0afce doc-src/TutorialI/Types/document/Numbers.tex
--- 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
diff -r 991ecdd985d9 -r 02cf78f0afce doc-src/TutorialI/isabelle.sty
--- 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}