--- 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));
--- 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%
--- 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 {
--- 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;
--- 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;
--- 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:%
--- 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%