# HG changeset patch
# User wenzelm
# Date 1198181378 -3600
# Node ID b3e415b0cf5c13a5a96ee6debb2e015c0f20474d
# Parent  41ff733fc76d79ab052e0c411fe382470dbef74a
updated;

diff -r 41ff733fc76d -r b3e415b0cf5c doc-src/IsarAdvanced/Classes/Thy/code_examples/Classes.hs
--- a/doc-src/IsarAdvanced/Classes/Thy/code_examples/Classes.hs	Thu Dec 20 14:33:43 2007 +0100
+++ b/doc-src/IsarAdvanced/Classes/Thy/code_examples/Classes.hs	Thu Dec 20 21:09:38 2007 +0100
@@ -50,11 +50,11 @@
   inverse = inverse_int;
 };
 
-pow_nat :: (Monoid a) => Nat -> a -> a;
+pow_nat :: forall a. (Monoid a) => Nat -> a -> a;
 pow_nat (Suc n) x = mult x (pow_nat n x);
 pow_nat Zero_nat x = neutral;
 
-pow_int :: (Group a) => Integer -> a -> a;
+pow_int :: forall a. (Group a) => Integer -> a -> a;
 pow_int k x =
   (if 0 <= k then pow_nat (nat k) x
     else inverse (pow_nat (nat (negate k)) x));
diff -r 41ff733fc76d -r b3e415b0cf5c doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Thu Dec 20 14:33:43 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Thu Dec 20 21:09:38 2007 +0100
@@ -461,7 +461,7 @@
 \ \ {\isachardoublequoteopen}head\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ null{\isachardoublequoteclose}\isanewline
 \ \ {\isacharbar}\ {\isachardoublequoteopen}head\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ {\isacharequal}\ x{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
-We provide some instances for our \isa{null}:%
+\noindent  We provide some instances for our \isa{null}:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{instantiation}\isamarkupfalse%
@@ -474,7 +474,7 @@
 \isanewline
 \isacommand{definition}\isamarkupfalse%
 \isanewline
-\ \ {\isachardoublequoteopen}null\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}null\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
 \isanewline
 \isacommand{instance}\isamarkupfalse%
 %
@@ -496,7 +496,7 @@
 \isacommand{end}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
-Constructing a dummy example:%
+\noindent Constructing a dummy example:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{definition}\isamarkupfalse%
diff -r 41ff733fc76d -r b3e415b0cf5c doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs	Thu Dec 20 14:33:43 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs	Thu Dec 20 21:09:38 2007 +0100
@@ -6,11 +6,11 @@
   nulla :: a;
 };
 
-heada :: (Codegen.Null a) => [a] -> a;
+heada :: forall a. (Codegen.Null a) => [a] -> a;
 heada (x : xs) = x;
 heada [] = Codegen.nulla;
 
-null_option :: Maybe a;
+null_option :: forall a. Maybe a;
 null_option = Nothing;
 
 instance Codegen.Null (Maybe a) where {
diff -r 41ff733fc76d -r b3e415b0cf5c doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML	Thu Dec 20 14:33:43 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML	Thu Dec 20 21:09:38 2007 +0100
@@ -3,10 +3,10 @@
 
 datatype nat = Suc of nat | Zero_nat;
 
-fun eqop_nat Zero_nat (Suc m) = false
-  | eqop_nat (Suc n) Zero_nat = false
-  | eqop_nat (Suc n) (Suc m) = eqop_nat n m
-  | eqop_nat Zero_nat Zero_nat = true;
+fun eqop_nat Zero_nat Zero_nat = true
+  | eqop_nat (Suc m) (Suc n) = eqop_nat m n
+  | eqop_nat Zero_nat (Suc a) = false
+  | eqop_nat (Suc a) Zero_nat = false;
 
 fun plus_nat (Suc m) n = plus_nat m (Suc n)
   | plus_nat Zero_nat n = n;
diff -r 41ff733fc76d -r b3e415b0cf5c doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML	Thu Dec 20 14:33:43 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML	Thu Dec 20 21:09:38 2007 +0100
@@ -26,10 +26,10 @@
 
 datatype nat = Suc of nat | Zero_nat;
 
-fun eqop_nat Zero_nat (Suc m) = false
-  | eqop_nat (Suc n) Zero_nat = false
-  | eqop_nat (Suc n) (Suc m) = eqop_nat n m
-  | eqop_nat Zero_nat Zero_nat = true;
+fun eqop_nat Zero_nat Zero_nat = true
+  | eqop_nat (Suc m) (Suc n) = eqop_nat m n
+  | eqop_nat Zero_nat (Suc a) = false
+  | eqop_nat (Suc a) Zero_nat = false;
 
 val eq_nat = {eqop = eqop_nat} : nat HOL.eq;
 
diff -r 41ff733fc76d -r b3e415b0cf5c doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex
--- a/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex	Thu Dec 20 14:33:43 2007 +0100
+++ b/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex	Thu Dec 20 21:09:38 2007 +0100
@@ -1792,11 +1792,8 @@
   list functions \isa{rev} and \isa{map}:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{function}\isamarkupfalse%
-\ mirror\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ tree\ {\isasymRightarrow}\ {\isacharprime}a\ tree{\isachardoublequoteclose}\isanewline
-\isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}mirror\ {\isacharparenleft}Leaf\ n{\isacharparenright}\ {\isacharequal}\ Leaf\ n{\isachardoublequoteclose}\isanewline
-{\isacharbar}\ {\isachardoublequoteopen}mirror\ {\isacharparenleft}Branch\ l{\isacharparenright}\ {\isacharequal}\ Branch\ {\isacharparenleft}rev\ {\isacharparenleft}map\ mirror\ l{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymin}\ set\ l\ {\isasymLongrightarrow}\ f\ x\ {\isacharless}\ Suc\ {\isacharparenleft}list{\isacharunderscore}size\ f\ l{\isacharparenright}{\isachardoublequoteclose}\isanewline
 %
 \isadelimproof
 %
@@ -1804,17 +1801,24 @@
 %
 \isatagproof
 \isacommand{by}\isamarkupfalse%
-\ pat{\isacharunderscore}completeness\ auto%
+\ {\isacharparenleft}induct\ l{\isacharparenright}\ auto%
 \endisatagproof
 {\isafoldproof}%
 %
 \isadelimproof
+\isanewline
 %
 \endisadelimproof
-%
+\isanewline
+\isanewline
+\isacommand{fun}\isamarkupfalse%
+\ mirror\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ tree\ {\isasymRightarrow}\ {\isacharprime}a\ tree{\isachardoublequoteclose}\isanewline
+\isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}mirror\ {\isacharparenleft}Leaf\ n{\isacharparenright}\ {\isacharequal}\ Leaf\ n{\isachardoublequoteclose}\isanewline
+{\isacharbar}\ {\isachardoublequoteopen}mirror\ {\isacharparenleft}Branch\ l{\isacharparenright}\ {\isacharequal}\ Branch\ {\isacharparenleft}rev\ {\isacharparenleft}map\ mirror\ l{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
-We do the termination proof manually, to point out what happens
-  here:%
+\emph{Note: The handling of size functions is currently changing 
+  in the developers version of Isabelle. So this documentation is outdated.}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{termination}\isamarkupfalse%
@@ -1860,7 +1864,7 @@
 Simplification returns the following subgoal: 
 
       \begin{isabelle}%
-{\isadigit{1}}{\isachardot}\ x\ {\isasymin}\ set\ l\ {\isasymLongrightarrow}\ size\ x\ {\isacharless}\ Suc\ {\isacharparenleft}tree{\isacharunderscore}list{\isacharunderscore}size\ l{\isacharparenright}%
+{\isadigit{1}}{\isachardot}\ x\ {\isasymin}\ set\ l\ {\isasymLongrightarrow}\ size\ x\ {\isacharless}\ Suc\ {\isacharparenleft}list{\isacharunderscore}size\ size\ l{\isacharparenright}%
 \end{isabelle} 
 
       We are lacking a property about the function \isa{tree{\isacharunderscore}list{\isacharunderscore}size}, which was generated automatically at the
@@ -1875,24 +1879,6 @@
 \isadelimproof
 %
 \endisadelimproof
-\isanewline
-\isacommand{lemma}\isamarkupfalse%
-\ tree{\isacharunderscore}list{\isacharunderscore}size{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ \isanewline
-\ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ l\ {\isasymLongrightarrow}\ size\ x\ {\isacharless}\ Suc\ {\isacharparenleft}tree{\isacharunderscore}list{\isacharunderscore}size\ l{\isacharparenright}{\isachardoublequoteclose}\isanewline
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}induct\ l{\isacharparenright}\ auto%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
 %
 \begin{isamarkuptext}%
 Now the whole termination proof is automatic:%
diff -r 41ff733fc76d -r b3e415b0cf5c doc-src/LaTeXsugar/Sugar/document/Sugar.tex
--- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Thu Dec 20 14:33:43 2007 +0100
+++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Thu Dec 20 21:09:38 2007 +0100
@@ -344,7 +344,7 @@
 the body of
 \newtheorem{theorem}{Theorem}
 \begin{theorem}
-\isa{{\rmfamily\upshape\normalsize{}If\,}\ \mbox{i\ {\isasymle}\ j}\ {\rmfamily\upshape\normalsize \,and\,}\ \mbox{j\ {\isasymle}\ k}\ {\rmfamily\upshape\normalsize \,then\,}\ i\ {\isasymle}\ k{\isachardot}}
+\isa{{\normalsize{}If\,}\ \mbox{i\ {\isasymle}\ j}\ {\normalsize \,and\,}\ \mbox{j\ {\isasymle}\ k}\ {\normalsize \,then\,}\ i\ {\isasymle}\ k{\isachardot}}
 \end{theorem}
 by typing
 \begin{quote}
@@ -354,12 +354,12 @@
 In order to prevent odd line breaks, the premises are put into boxes.
 At times this is too drastic:
 \begin{theorem}
-\isa{{\rmfamily\upshape\normalsize{}If\,}\ \mbox{longpremise}\ {\rmfamily\upshape\normalsize \,and\,}\ \mbox{longerpremise}\ {\rmfamily\upshape\normalsize \,and\,}\ \mbox{P\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ x{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}}\ {\rmfamily\upshape\normalsize \,and\,}\ \mbox{longestpremise}\ {\rmfamily\upshape\normalsize \,then\,}\ conclusion{\isachardot}}
+\isa{{\normalsize{}If\,}\ \mbox{longpremise}\ {\normalsize \,and\,}\ \mbox{longerpremise}\ {\normalsize \,and\,}\ \mbox{P\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ x{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}}\ {\normalsize \,and\,}\ \mbox{longestpremise}\ {\normalsize \,then\,}\ conclusion{\isachardot}}
 \end{theorem}
 In which case you should use \texttt{IfThenNoBox} instead of
 \texttt{IfThen}:
 \begin{theorem}
-\isa{{\rmfamily\upshape\normalsize{}If\,}\ longpremise\ {\rmfamily\upshape\normalsize \,and\,}\ longerpremise\ {\rmfamily\upshape\normalsize \,and\,}\ P\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ x{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\rmfamily\upshape\normalsize \,and\,}\ longestpremise\ {\rmfamily\upshape\normalsize \,then\,}\ conclusion{\isachardot}}
+\isa{{\normalsize{}If\,}\ longpremise\ {\normalsize \,and\,}\ longerpremise\ {\normalsize \,and\,}\ P\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ x{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\normalsize \,and\,}\ longestpremise\ {\normalsize \,then\,}\ conclusion{\isachardot}}
 \end{theorem}%
 \end{isamarkuptext}%
 \isamarkuptrue%