merged
authorwenzelm
Thu, 02 Apr 2009 13:41:31 +0200
changeset 30846 fd8ed5a39a8e
parent 30844 7d0e10a961a6 (diff)
parent 30845 9a887484de53 (current diff)
child 30847 dd9a1662413b
merged
--- a/doc-src/Classes/Thy/document/Classes.tex	Thu Apr 02 13:41:02 2009 +0200
+++ b/doc-src/Classes/Thy/document/Classes.tex	Thu Apr 02 13:41:31 2009 +0200
@@ -1191,7 +1191,7 @@
 \hspace*{0pt}\\
 \hspace*{0pt}pow{\char95}nat ::~forall a.~(Monoid a) => Nat -> a -> a;\\
 \hspace*{0pt}pow{\char95}nat Zero{\char95}nat x = neutral;\\
-\hspace*{0pt}pow{\char95}nat (Suc n) xa = mult xa (pow{\char95}nat n xa);\\
+\hspace*{0pt}pow{\char95}nat (Suc n) x = mult x (pow{\char95}nat n x);\\
 \hspace*{0pt}\\
 \hspace*{0pt}pow{\char95}int ::~forall a.~(Group a) => Integer -> a -> a;\\
 \hspace*{0pt}pow{\char95}int k x =\\
@@ -1272,8 +1272,8 @@
 \hspace*{0pt} ~IntInf.int group;\\
 \hspace*{0pt}\\
 \hspace*{0pt}fun pow{\char95}nat A{\char95}~Zero{\char95}nat x = neutral (monoidl{\char95}monoid A{\char95})\\
-\hspace*{0pt} ~| pow{\char95}nat A{\char95}~(Suc n) xa =\\
-\hspace*{0pt} ~~~mult ((semigroup{\char95}monoidl o monoidl{\char95}monoid) A{\char95}) xa (pow{\char95}nat A{\char95}~n xa);\\
+\hspace*{0pt} ~| pow{\char95}nat A{\char95}~(Suc n) x =\\
+\hspace*{0pt} ~~~mult ((semigroup{\char95}monoidl o monoidl{\char95}monoid) A{\char95}) x (pow{\char95}nat A{\char95}~n x);\\
 \hspace*{0pt}\\
 \hspace*{0pt}fun pow{\char95}int A{\char95}~k x =\\
 \hspace*{0pt} ~(if IntInf.<= ((0 :~IntInf.int),~k)\\
--- a/doc-src/Codegen/Thy/Adaption.thy	Thu Apr 02 13:41:02 2009 +0200
+++ b/doc-src/Codegen/Thy/Adaption.thy	Thu Apr 02 13:41:31 2009 +0200
@@ -59,42 +59,7 @@
   supposed to be:
 
   \begin{figure}[here]
-    \begin{tikzpicture}[scale = 0.5]
-      \tikzstyle water=[color = blue, thick]
-      \tikzstyle ice=[color = black, very thick, cap = round, join = round, fill = white]
-      \tikzstyle process=[color = green, semithick, ->]
-      \tikzstyle adaption=[color = red, semithick, ->]
-      \tikzstyle target=[color = black]
-      \foreach \x in {0, ..., 24}
-        \draw[style=water] (\x, 0.25) sin + (0.25, 0.25) cos + (0.25, -0.25) sin
-          + (0.25, -0.25) cos + (0.25, 0.25);
-      \draw[style=ice] (1, 0) --
-        (3, 6) node[above, fill=white] {logic} -- (5, 0) -- cycle;
-      \draw[style=ice] (9, 0) --
-        (11, 6) node[above, fill=white] {intermediate language} -- (13, 0) -- cycle;
-      \draw[style=ice] (15, -6) --
-        (19, 6) node[above, fill=white] {target language} -- (23, -6) -- cycle;
-      \draw[style=process]
-        (3.5, 3) .. controls (7, 5) .. node[fill=white] {translation} (10.5, 3);
-      \draw[style=process]
-        (11.5, 3) .. controls (15, 5) .. node[fill=white] (serialisation) {serialisation} (18.5, 3);
-      \node (adaption) at (11, -2) [style=adaption] {adaption};
-      \node at (19, 3) [rotate=90] {generated};
-      \node at (19.5, -5) {language};
-      \node at (19.5, -3) {library};
-      \node (includes) at (19.5, -1) {includes};
-      \node (reserved) at (16.5, -3) [rotate=72] {reserved}; % proper 71.57
-      \draw[style=process]
-        (includes) -- (serialisation);
-      \draw[style=process]
-        (reserved) -- (serialisation);
-      \draw[style=adaption]
-        (adaption) -- (serialisation);
-      \draw[style=adaption]
-        (adaption) -- (includes);
-      \draw[style=adaption]
-        (adaption) -- (reserved);
-    \end{tikzpicture}
+    \includegraphics{Thy/pictures/adaption}
     \caption{The adaption principle}
     \label{fig:adaption}
   \end{figure}
--- a/doc-src/Codegen/Thy/Introduction.thy	Thu Apr 02 13:41:02 2009 +0200
+++ b/doc-src/Codegen/Thy/Introduction.thy	Thu Apr 02 13:41:31 2009 +0200
@@ -121,29 +121,7 @@
   how it works.
 
   \begin{figure}[h]
-    \begin{tikzpicture}[x = 4.2cm, y = 1cm]
-      \tikzstyle entity=[rounded corners, draw, thick, color = black, fill = white];
-      \tikzstyle process=[ellipse, draw, thick, color = green, fill = white];
-      \tikzstyle process_arrow=[->, semithick, color = green];
-      \node (HOL) at (0, 4) [style=entity] {@{text "Isabelle/HOL"} theory};
-      \node (eqn) at (2, 2) [style=entity] {code equations};
-      \node (iml) at (2, 0) [style=entity] {intermediate language};
-      \node (seri) at (1, 0) [style=process] {serialisation};
-      \node (SML) at (0, 3) [style=entity] {@{text SML}};
-      \node (OCaml) at (0, 2) [style=entity] {@{text OCaml}};
-      \node (further) at (0, 1) [style=entity] {@{text "\<dots>"}};
-      \node (Haskell) at (0, 0) [style=entity] {@{text Haskell}};
-      \draw [style=process_arrow] (HOL) .. controls (2, 4) ..
-        node [style=process, near start] {selection}
-        node [style=process, near end] {preprocessing}
-        (eqn);
-      \draw [style=process_arrow] (eqn) -- node (transl) [style=process] {translation} (iml);
-      \draw [style=process_arrow] (iml) -- (seri);
-      \draw [style=process_arrow] (seri) -- (SML);
-      \draw [style=process_arrow] (seri) -- (OCaml);
-      \draw [style=process_arrow, dashed] (seri) -- (further);
-      \draw [style=process_arrow] (seri) -- (Haskell);
-    \end{tikzpicture}
+    \includegraphics{Thy/pictures/architecture}
     \caption{Code generator architecture}
     \label{fig:arch}
   \end{figure}
@@ -164,35 +142,29 @@
 
   \begin{itemize}
 
-    \item Out of the vast collection of theorems proven in a
-      \qn{theory}, a reasonable subset modelling
-      code equations is \qn{selected}.
-
-    \item On those selected theorems, certain
-      transformations are carried out
-      (\qn{preprocessing}).  Their purpose is to turn theorems
-      representing non- or badly executable
-      specifications into equivalent but executable counterparts.
-      The result is a structured collection of \qn{code theorems}.
+    \item Starting point is a collection of raw code equations in a
+      theory; due to proof irrelevance it is not relevant where they
+      stem from but typically they are either descendant of specification
+      tools or explicit proofs by the user.
+      
+    \item Before these raw code equations are continued
+      with, they can be subjected to theorem transformations.  This
+      \qn{preprocessor} is an interface which allows to apply the full
+      expressiveness of ML-based theorem transformations to code
+      generation.  The result of the preprocessing step is a
+      structured collection of code equations.
 
-    \item Before the selected code equations are continued with,
-      they can be \qn{preprocessed}, i.e. subjected to theorem
-      transformations.  This \qn{preprocessor} is an interface which
-      allows to apply
-      the full expressiveness of ML-based theorem transformations
-      to code generation;  motivating examples are shown below, see
-      \secref{sec:preproc}.
-      The result of the preprocessing step is a structured collection
-      of code equations.
-
-    \item These code equations are \qn{translated} to a program
-      in an abstract intermediate language.  Think of it as a kind
+    \item These code equations are \qn{translated} to a program in an
+      abstract intermediate language.  Think of it as a kind
       of \qt{Mini-Haskell} with four \qn{statements}: @{text data}
       (for datatypes), @{text fun} (stemming from code equations),
       also @{text class} and @{text inst} (for type classes).
 
     \item Finally, the abstract program is \qn{serialised} into concrete
       source code of a target language.
+      This step only produces concrete syntax but does not change the
+      program in essence; all conceptual transformations occur in the
+      translation step.
 
   \end{itemize}
 
--- a/doc-src/Codegen/Thy/document/Adaption.tex	Thu Apr 02 13:41:02 2009 +0200
+++ b/doc-src/Codegen/Thy/document/Adaption.tex	Thu Apr 02 13:41:31 2009 +0200
@@ -96,42 +96,7 @@
   supposed to be:
 
   \begin{figure}[here]
-    \begin{tikzpicture}[scale = 0.5]
-      \tikzstyle water=[color = blue, thick]
-      \tikzstyle ice=[color = black, very thick, cap = round, join = round, fill = white]
-      \tikzstyle process=[color = green, semithick, ->]
-      \tikzstyle adaption=[color = red, semithick, ->]
-      \tikzstyle target=[color = black]
-      \foreach \x in {0, ..., 24}
-        \draw[style=water] (\x, 0.25) sin + (0.25, 0.25) cos + (0.25, -0.25) sin
-          + (0.25, -0.25) cos + (0.25, 0.25);
-      \draw[style=ice] (1, 0) --
-        (3, 6) node[above, fill=white] {logic} -- (5, 0) -- cycle;
-      \draw[style=ice] (9, 0) --
-        (11, 6) node[above, fill=white] {intermediate language} -- (13, 0) -- cycle;
-      \draw[style=ice] (15, -6) --
-        (19, 6) node[above, fill=white] {target language} -- (23, -6) -- cycle;
-      \draw[style=process]
-        (3.5, 3) .. controls (7, 5) .. node[fill=white] {translation} (10.5, 3);
-      \draw[style=process]
-        (11.5, 3) .. controls (15, 5) .. node[fill=white] (serialisation) {serialisation} (18.5, 3);
-      \node (adaption) at (11, -2) [style=adaption] {adaption};
-      \node at (19, 3) [rotate=90] {generated};
-      \node at (19.5, -5) {language};
-      \node at (19.5, -3) {library};
-      \node (includes) at (19.5, -1) {includes};
-      \node (reserved) at (16.5, -3) [rotate=72] {reserved}; % proper 71.57
-      \draw[style=process]
-        (includes) -- (serialisation);
-      \draw[style=process]
-        (reserved) -- (serialisation);
-      \draw[style=adaption]
-        (adaption) -- (serialisation);
-      \draw[style=adaption]
-        (adaption) -- (includes);
-      \draw[style=adaption]
-        (adaption) -- (reserved);
-    \end{tikzpicture}
+    \includegraphics{Thy/pictures/adaption}
     \caption{The adaption principle}
     \label{fig:adaption}
   \end{figure}
--- a/doc-src/Codegen/Thy/document/Introduction.tex	Thu Apr 02 13:41:02 2009 +0200
+++ b/doc-src/Codegen/Thy/document/Introduction.tex	Thu Apr 02 13:41:31 2009 +0200
@@ -284,29 +284,7 @@
   how it works.
 
   \begin{figure}[h]
-    \begin{tikzpicture}[x = 4.2cm, y = 1cm]
-      \tikzstyle entity=[rounded corners, draw, thick, color = black, fill = white];
-      \tikzstyle process=[ellipse, draw, thick, color = green, fill = white];
-      \tikzstyle process_arrow=[->, semithick, color = green];
-      \node (HOL) at (0, 4) [style=entity] {\isa{Isabelle{\isacharslash}HOL} theory};
-      \node (eqn) at (2, 2) [style=entity] {code equations};
-      \node (iml) at (2, 0) [style=entity] {intermediate language};
-      \node (seri) at (1, 0) [style=process] {serialisation};
-      \node (SML) at (0, 3) [style=entity] {\isa{SML}};
-      \node (OCaml) at (0, 2) [style=entity] {\isa{OCaml}};
-      \node (further) at (0, 1) [style=entity] {\isa{{\isasymdots}}};
-      \node (Haskell) at (0, 0) [style=entity] {\isa{Haskell}};
-      \draw [style=process_arrow] (HOL) .. controls (2, 4) ..
-        node [style=process, near start] {selection}
-        node [style=process, near end] {preprocessing}
-        (eqn);
-      \draw [style=process_arrow] (eqn) -- node (transl) [style=process] {translation} (iml);
-      \draw [style=process_arrow] (iml) -- (seri);
-      \draw [style=process_arrow] (seri) -- (SML);
-      \draw [style=process_arrow] (seri) -- (OCaml);
-      \draw [style=process_arrow, dashed] (seri) -- (further);
-      \draw [style=process_arrow] (seri) -- (Haskell);
-    \end{tikzpicture}
+    \includegraphics{Thy/pictures/architecture}
     \caption{Code generator architecture}
     \label{fig:arch}
   \end{figure}
@@ -327,35 +305,29 @@
 
   \begin{itemize}
 
-    \item Out of the vast collection of theorems proven in a
-      \qn{theory}, a reasonable subset modelling
-      code equations is \qn{selected}.
-
-    \item On those selected theorems, certain
-      transformations are carried out
-      (\qn{preprocessing}).  Their purpose is to turn theorems
-      representing non- or badly executable
-      specifications into equivalent but executable counterparts.
-      The result is a structured collection of \qn{code theorems}.
+    \item Starting point is a collection of raw code equations in a
+      theory; due to proof irrelevance it is not relevant where they
+      stem from but typically they are either descendant of specification
+      tools or explicit proofs by the user.
+      
+    \item Before these raw code equations are continued
+      with, they can be subjected to theorem transformations.  This
+      \qn{preprocessor} is an interface which allows to apply the full
+      expressiveness of ML-based theorem transformations to code
+      generation.  The result of the preprocessing step is a
+      structured collection of code equations.
 
-    \item Before the selected code equations are continued with,
-      they can be \qn{preprocessed}, i.e. subjected to theorem
-      transformations.  This \qn{preprocessor} is an interface which
-      allows to apply
-      the full expressiveness of ML-based theorem transformations
-      to code generation;  motivating examples are shown below, see
-      \secref{sec:preproc}.
-      The result of the preprocessing step is a structured collection
-      of code equations.
-
-    \item These code equations are \qn{translated} to a program
-      in an abstract intermediate language.  Think of it as a kind
+    \item These code equations are \qn{translated} to a program in an
+      abstract intermediate language.  Think of it as a kind
       of \qt{Mini-Haskell} with four \qn{statements}: \isa{data}
       (for datatypes), \isa{fun} (stemming from code equations),
       also \isa{class} and \isa{inst} (for type classes).
 
     \item Finally, the abstract program is \qn{serialised} into concrete
       source code of a target language.
+      This step only produces concrete syntax but does not change the
+      program in essence; all conceptual transformations occur in the
+      translation step.
 
   \end{itemize}
 
--- a/doc-src/Codegen/Thy/pictures/adaption.tex	Thu Apr 02 13:41:02 2009 +0200
+++ b/doc-src/Codegen/Thy/pictures/adaption.tex	Thu Apr 02 13:41:31 2009 +0200
@@ -1,7 +1,5 @@
 
 \documentclass[12pt]{article}
-\usepackage{pgf}
-\usepackage{pgflibraryshapes}
 \usepackage{tikz}
 
 \begin{document}
@@ -10,7 +8,7 @@
 \setlength{\fboxrule}{0.01pt}
 \setlength{\fboxsep}{4pt}
 
-\fbox{
+\fcolorbox{white}{white}{
 
 \begin{tikzpicture}[scale = 0.5]
   \tikzstyle water=[color = blue, thick]
--- a/doc-src/Codegen/Thy/pictures/architecture.tex	Thu Apr 02 13:41:02 2009 +0200
+++ b/doc-src/Codegen/Thy/pictures/architecture.tex	Thu Apr 02 13:41:31 2009 +0200
@@ -1,8 +1,8 @@
 
 \documentclass[12pt]{article}
-\usepackage{pgf}
-\usepackage{pgflibraryshapes}
 \usepackage{tikz}
+\usetikzlibrary{shapes}
+\usetikzlibrary{arrows}
 
 \begin{document}
 
@@ -10,30 +10,39 @@
 \setlength{\fboxrule}{0.01pt}
 \setlength{\fboxsep}{4pt}
 
-\fbox{
+\fcolorbox{white}{white}{
+
+\newcommand{\sys}[1]{\emph{#1}}
 
-\begin{tikzpicture}[x = 4.2cm, y = 1cm]
-  \tikzstyle entity=[rounded corners, draw, thick, color = black, fill = white];
-  \tikzstyle process=[ellipse, draw, thick, color = green, fill = white];
-  \tikzstyle process_arrow=[->, semithick, color = green];
-  \node (HOL) at (0, 4) [style=entity] {Isabelle/HOL theory};
-  \node (eqn) at (2, 2) [style=entity] {code equations};
-  \node (iml) at (2, 0) [style=entity] {intermediate language};
-  \node (seri) at (1, 0) [style=process] {serialisation};
-  \node (SML) at (0, 3) [style=entity] {SML};
-  \node (OCaml) at (0, 2) [style=entity] {OCaml};
-  \node (further) at (0, 1) [style=entity] {\ldots};
-  \node (Haskell) at (0, 0) [style=entity] {Haskell};
-  \draw [style=process_arrow] (HOL) .. controls (2, 4) ..
-    node [style=process, near start] {selection}
-    node [style=process, near end] {preprocessing}
-    (eqn);
-  \draw [style=process_arrow] (eqn) -- node (transl) [style=process] {translation} (iml);
-  \draw [style=process_arrow] (iml) -- (seri);
-  \draw [style=process_arrow] (seri) -- (SML);
-  \draw [style=process_arrow] (seri) -- (OCaml);
-  \draw [style=process_arrow, dashed] (seri) -- (further);
-  \draw [style=process_arrow] (seri) -- (Haskell);
+\begin{tikzpicture}[x = 4cm, y = 1cm]
+  \tikzstyle positive=[color = black, fill = white];
+  \tikzstyle negative=[color = white, fill = black];
+  \tikzstyle entity=[rounded corners, draw, thick];
+  \tikzstyle process=[ellipse, draw, thick];
+  \tikzstyle arrow=[-stealth, semithick];
+  \node (spec) at (0, 3) [entity, positive] {specification tools};
+  \node (user) at (1, 3) [entity, positive] {user proofs};
+  \node (spec_user_join) at (0.5, 3) [shape=coordinate] {};
+  \node (raw) at (0.5, 4) [entity, positive] {raw code equations};
+  \node (pre) at (1.5, 4) [process, positive] {preprocessing};
+  \node (eqn) at (2.5, 4) [entity, positive] {code equations};
+  \node (iml) at (0.5, 0) [entity, positive] {intermediate program};
+  \node (seri) at (1.5, 0) [process, positive] {serialisation};
+  \node (SML) at (2.5, 3) [entity, positive] {\sys{SML}};
+  \node (OCaml) at (2.5, 2) [entity, positive] {\sys{OCaml}};
+  \node (further) at (2.5, 1) [entity, positive] {(\ldots)};
+  \node (Haskell) at (2.5, 0) [entity, positive] {\sys{Haskell}};
+  \draw [semithick] (spec) -- (spec_user_join);
+  \draw [semithick] (user) -- (spec_user_join);
+  \draw [-diamond, semithick] (spec_user_join) -- (raw);
+  \draw [arrow] (raw) -- (pre);
+  \draw [arrow] (pre) -- (eqn);
+  \draw [arrow] (eqn) -- node (transl) [process, positive] {translation} (iml);
+  \draw [arrow] (iml) -- (seri);
+  \draw [arrow] (seri) -- (SML);
+  \draw [arrow] (seri) -- (OCaml);
+  \draw [arrow, dashed] (seri) -- (further);
+  \draw [arrow] (seri) -- (Haskell);
 \end{tikzpicture}
 
 }
--- a/doc-src/Codegen/codegen.tex	Thu Apr 02 13:41:02 2009 +0200
+++ b/doc-src/Codegen/codegen.tex	Thu Apr 02 13:41:31 2009 +0200
@@ -5,9 +5,6 @@
 \usepackage{../iman,../extra,../isar,../proof}
 \usepackage{../isabelle,../isabellesym}
 \usepackage{style}
-\usepackage{pgf}
-\usepackage{pgflibraryshapes}
-\usepackage{tikz}
 \usepackage{../pdfsetup}
 
 \hyphenation{Isabelle}
--- a/src/HOL/Divides.thy	Thu Apr 02 13:41:02 2009 +0200
+++ b/src/HOL/Divides.thy	Thu Apr 02 13:41:31 2009 +0200
@@ -238,6 +238,10 @@
     by (simp only: mod_add_eq [symmetric])
 qed
 
+lemma div_add[simp]: "z dvd x \<Longrightarrow> z dvd y
+  \<Longrightarrow> (x + y) div z = x div z + y div z"
+by(cases "z=0", simp, unfold dvd_def, auto simp add: algebra_simps)
+
 text {* Multiplication respects modular equivalence. *}
 
 lemma mod_mult_left_eq: "(a * b) mod c = ((a mod c) * b) mod c"
@@ -765,7 +769,7 @@
 
 
 (* Monotonicity of div in first argument *)
-lemma div_le_mono [rule_format (no_asm)]:
+lemma div_le_mono [rule_format]:
     "\<forall>m::nat. m \<le> n --> (m div k) \<le> (n div k)"
 apply (case_tac "k=0", simp)
 apply (induct "n" rule: nat_less_induct, clarify)
@@ -820,6 +824,12 @@
   apply (simp_all)
 done
 
+lemma nat_div_eq_0 [simp]: "(n::nat) > 0 ==> ((m div n) = 0) = (m < n)"
+by(auto, subst mod_div_equality [of m n, symmetric], auto)
+
+lemma nat_div_gt_0 [simp]: "(n::nat) > 0 ==> ((m div n) > 0) = (m >= n)"
+by (subst neq0_conv [symmetric], auto)
+
 declare div_less_dividend [simp]
 
 text{*A fact for the mutilated chess board*}
@@ -905,13 +915,10 @@
   done
 
 lemma dvd_imp_le: "[| k dvd n; 0 < n |] ==> k \<le> (n::nat)"
-  apply (unfold dvd_def, clarify)
-  apply (simp_all (no_asm_use) add: zero_less_mult_iff)
-  apply (erule conjE)
-  apply (rule le_trans)
-   apply (rule_tac [2] le_refl [THEN mult_le_mono])
-   apply (erule_tac [2] Suc_leI, simp)
-  done
+by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
+
+lemma nat_dvd_not_less: "(0::nat) < m \<Longrightarrow> m < n \<Longrightarrow> \<not> n dvd m"
+by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
 
 lemma dvd_mult_div_cancel: "n dvd m ==> n * (m div n) = (m::nat)"
   apply (subgoal_tac "m mod n = 0")
@@ -1148,9 +1155,4 @@
   with j show ?thesis by blast
 qed
 
-lemma nat_dvd_not_less:
-  fixes m n :: nat
-  shows "0 < m \<Longrightarrow> m < n \<Longrightarrow> \<not> n dvd m"
-by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
-
 end
--- a/src/HOL/Finite_Set.thy	Thu Apr 02 13:41:02 2009 +0200
+++ b/src/HOL/Finite_Set.thy	Thu Apr 02 13:41:31 2009 +0200
@@ -1084,10 +1084,8 @@
 qed
 
 lemma setsum_mono_zero_right: 
-  assumes fT: "finite T" and ST: "S \<subseteq> T"
-  and z: "\<forall>i \<in> T - S. f i = 0"
-  shows "setsum f T = setsum f S"
-using setsum_mono_zero_left[OF fT ST z] by simp
+  "finite T \<Longrightarrow> S \<subseteq> T \<Longrightarrow> \<forall>i \<in> T - S. f i = 0 \<Longrightarrow> setsum f T = setsum f S"
+by(blast intro!: setsum_mono_zero_left[symmetric])
 
 lemma setsum_mono_zero_cong_left: 
   assumes fT: "finite T" and ST: "S \<subseteq> T"
@@ -1645,7 +1643,7 @@
   "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
 by(fastsimp simp: setprod_def intro: fold_image_cong)
 
-lemma strong_setprod_cong:
+lemma strong_setprod_cong[cong]:
   "A = B ==> (!!x. x:B =simp=> f x = g x) ==> setprod f A = setprod g B"
 by(fastsimp simp: simp_implies_def setprod_def intro: fold_image_cong)
 
@@ -1662,7 +1660,7 @@
     then show ?thesis apply simp
       apply (rule setprod_cong)
       apply simp
-      by (erule eq[symmetric])
+      by (simp add: eq)
 qed
 
 lemma setprod_Un_one:  
@@ -1694,6 +1692,20 @@
   ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
 by (subst setprod_Un_Int [symmetric], auto)
 
+lemma setprod_mono_one_left: 
+  assumes fT: "finite T" and ST: "S \<subseteq> T"
+  and z: "\<forall>i \<in> T - S. f i = 1"
+  shows "setprod f S = setprod f T"
+proof-
+  have eq: "T = S \<union> (T - S)" using ST by blast
+  have d: "S \<inter> (T - S) = {}" using ST by blast
+  from fT ST have f: "finite S" "finite (T - S)" by (auto intro: finite_subset)
+  show ?thesis
+  by (simp add: setprod_Un_disjoint[OF f d, unfolded eq[symmetric]] setprod_1'[OF z])
+qed
+
+lemmas setprod_mono_one_right = setprod_mono_one_left [THEN sym]
+
 lemma setprod_delta: 
   assumes fS: "finite S"
   shows "setprod (\<lambda>k. if k=a then b k else 1) S = (if a \<in> S then b a else 1)"
@@ -1776,49 +1788,26 @@
 done
 
 lemma setprod_nonneg [rule_format]:
-   "(ALL x: A. (0::'a::ordered_idom) \<le> f x) --> 0 \<le> setprod f A"
-apply (case_tac "finite A")
-apply (induct set: finite, force, clarsimp)
-apply (subgoal_tac "0 * 0 \<le> f x * setprod f F", force)
-apply (rule mult_mono, assumption+)
-apply (auto simp add: setprod_def)
-done
-
-lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::ordered_idom) < f x)
+   "(ALL x: A. (0::'a::ordered_semidom) \<le> f x) --> 0 \<le> setprod f A"
+by (cases "finite A", induct set: finite, simp_all add: mult_nonneg_nonneg)
+
+lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::ordered_semidom) < f x)
   --> 0 < setprod f A"
-apply (case_tac "finite A")
-apply (induct set: finite, force, clarsimp)
-apply (subgoal_tac "0 * 0 < f x * setprod f F", force)
-apply (rule mult_strict_mono, assumption+)
-apply (auto simp add: setprod_def)
-done
-
-lemma setprod_nonzero [rule_format]:
-  "(ALL x y. (x::'a::comm_semiring_1) * y = 0 --> x = 0 | y = 0) ==>
-    finite A ==> (ALL x: A. f x \<noteq> (0::'a)) --> setprod f A \<noteq> 0"
-by (erule finite_induct, auto)
-
-lemma setprod_zero_eq:
-    "(ALL x y. (x::'a::comm_semiring_1) * y = 0 --> x = 0 | y = 0) ==>
-     finite A ==> (setprod f A = (0::'a)) = (EX x: A. f x = 0)"
-by (insert setprod_zero [of A f] setprod_nonzero [of A f], blast)
-
-lemma setprod_nonzero_field:
-    "finite A ==> (ALL x: A. f x \<noteq> (0::'a::idom)) ==> setprod f A \<noteq> 0"
-by (rule setprod_nonzero, auto)
-
-lemma setprod_zero_eq_field:
-    "finite A ==> (setprod f A = (0::'a::idom)) = (EX x: A. f x = 0)"
-by (rule setprod_zero_eq, auto)
+by (cases "finite A", induct set: finite, simp_all add: mult_pos_pos)
+
+lemma setprod_zero_iff[simp]: "finite A ==> 
+  (setprod f A = (0::'a::{comm_semiring_1,no_zero_divisors})) =
+  (EX x: A. f x = 0)"
+by (erule finite_induct, auto simp:no_zero_divisors)
+
+lemma setprod_pos_nat:
+  "finite S ==> (ALL x : S. f x > (0::nat)) ==> setprod f S > 0"
+using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
 
 lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==>
   (setprod f (A Un B) :: 'a ::{field})
    = setprod f A * setprod f B / setprod f (A Int B)"
-apply (subst setprod_Un_Int [symmetric], auto)
-apply (subgoal_tac "finite (A Int B)")
-apply (frule setprod_nonzero_field [of "A Int B" f], assumption)
-apply (subst times_divide_eq_right [THEN sym], auto)
-done
+by (subst setprod_Un_Int [symmetric], auto)
 
 lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
   (setprod f (A - {a}) :: 'a :: {field}) =
--- a/src/HOL/Int.thy	Thu Apr 02 13:41:02 2009 +0200
+++ b/src/HOL/Int.thy	Thu Apr 02 13:41:31 2009 +0200
@@ -1382,8 +1382,6 @@
 
 subsection {* @{term setsum} and @{term setprod} *}
 
-text {*By Jeremy Avigad*}
-
 lemma of_nat_setsum: "of_nat (setsum f A) = (\<Sum>x\<in>A. of_nat(f x))"
   apply (cases "finite A")
   apply (erule finite_induct, auto)
@@ -1404,22 +1402,6 @@
   apply (erule finite_induct, auto)
   done
 
-lemma setprod_nonzero_nat:
-    "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::nat)) ==> setprod f A \<noteq> 0"
-  by (rule setprod_nonzero, auto)
-
-lemma setprod_zero_eq_nat:
-    "finite A ==> (setprod f A = (0::nat)) = (\<exists>x \<in> A. f x = 0)"
-  by (rule setprod_zero_eq, auto)
-
-lemma setprod_nonzero_int:
-    "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::int)) ==> setprod f A \<noteq> 0"
-  by (rule setprod_nonzero, auto)
-
-lemma setprod_zero_eq_int:
-    "finite A ==> (setprod f A = (0::int)) = (\<exists>x \<in> A. f x = 0)"
-  by (rule setprod_zero_eq, auto)
-
 lemmas int_setsum = of_nat_setsum [where 'a=int]
 lemmas int_setprod = of_nat_setprod [where 'a=int]
 
--- a/src/HOL/Library/Binomial.thy	Thu Apr 02 13:41:02 2009 +0200
+++ b/src/HOL/Library/Binomial.thy	Thu Apr 02 13:41:31 2009 +0200
@@ -267,8 +267,6 @@
   moreover
   {assume n0: "n \<noteq> 0"
     then have ?thesis apply (simp add: h pochhammer_Suc_setprod)
-  apply (rule iffD2[OF setprod_zero_eq])
-  apply auto
   apply (rule_tac x="n" in bexI)
   using h kn by auto}
 ultimately show ?thesis by blast
@@ -281,8 +279,7 @@
   moreover
   {fix h assume h: "k = Suc h"
     then have ?thesis apply (simp add: pochhammer_Suc_setprod)
-      apply (subst setprod_zero_eq_field)
-      using h kn by (auto simp add: ring_simps)}
+      using h kn by (auto simp add: algebra_simps)}
   ultimately show ?thesis by (cases k, auto)
 qed
 
@@ -299,15 +296,14 @@
   where "a gchoose n = (if n = 0 then 1 else (setprod (\<lambda>i. a - of_nat i) {0 .. n - 1}) / of_nat (fact n))"
 
 lemma gbinomial_0[simp]: "a gchoose 0 = 1" "0 gchoose (Suc n) = 0"
-  apply (simp_all add: gbinomial_def)
-  apply (subgoal_tac "(\<Prod>i\<Colon>nat\<in>{0\<Colon>nat..n}. - of_nat i) = (0::'b)")
-  apply simp
-  apply (rule iffD2[OF setprod_zero_eq])
-  by auto
+apply (simp_all add: gbinomial_def)
+apply (subgoal_tac "(\<Prod>i\<Colon>nat\<in>{0\<Colon>nat..n}. - of_nat i) = (0::'b)")
+ apply (simp del:setprod_zero_iff)
+apply simp
+done
 
 lemma gbinomial_pochhammer: "a gchoose n = (- 1) ^ n * pochhammer (- a) n / of_nat (fact n)"
 proof-
-
   {assume "n=0" then have ?thesis by simp}
   moreover
   {assume n0: "n\<noteq>0"
@@ -388,7 +384,6 @@
       unfolding mult_assoc[symmetric] 
       unfolding setprod_timesf[symmetric]
       apply simp
-      apply (rule disjI2)
       apply (rule strong_setprod_reindex_cong[where f= "op - n"])
       apply (auto simp add: inj_on_def image_iff Bex_def)
       apply presburger
--- a/src/HOL/Library/Determinants.thy	Thu Apr 02 13:41:02 2009 +0200
+++ b/src/HOL/Library/Determinants.thy	Thu Apr 02 13:41:31 2009 +0200
@@ -106,7 +106,7 @@
   moreover
   {assume fS: "finite S"
     then have ?thesis
-      apply (simp add: setprod_def)
+      apply (simp add: setprod_def cong del:strong_setprod_cong)
       apply (rule ab_semigroup_mult.fold_image_permute)
       apply (auto simp add: p)
       apply unfold_locales
@@ -115,7 +115,7 @@
 qed
 
 lemma setproduct_permute_nat_interval: "p permutes {m::nat .. n} ==> setprod f {m..n} = setprod (f o p) {m..n}"
-  by (auto intro: setprod_permute)
+  by (blast intro!: setprod_permute)
 
 (* ------------------------------------------------------------------------- *)
 (* Basic determinant properties.                                             *)
@@ -310,10 +310,7 @@
 using r
 apply (simp add: row_def det_def Cart_eq)
 apply (rule setsum_0')
-apply (clarsimp simp add: sign_nz)
-apply (rule setprod_zero)
-apply simp
-apply auto
+apply (auto simp: sign_nz)
 done
 
 lemma det_zero_column:
--- a/src/HOL/Library/Formal_Power_Series.thy	Thu Apr 02 13:41:02 2009 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy	Thu Apr 02 13:41:31 2009 +0200
@@ -1289,10 +1289,6 @@
       apply auto
       unfolding setprod_Un_disjoint[OF f0 d0, unfolded u0, unfolded k]
       apply (clarsimp simp add: natpermute_def nth_append)
-      apply (rule_tac f="\<lambda>x. x * a (Suc k) $ (n - foldl op + 0 aa)" in cong[OF refl])
-      apply (rule setprod_cong)
-      apply simp
-      apply simp
       done
     finally have "?P m n" .}
   ultimately show "?P m n " by (cases m, auto)
@@ -1321,9 +1317,7 @@
   {fix n assume m: "m = Suc n"
     have c: "m = card {0..n}" using m by simp
    have "(a ^m)$0 = setprod (\<lambda>i. a$0) {0..n}"
-     apply (simp add: m fps_power_nth del: replicate.simps power_Suc)
-     apply (rule setprod_cong)
-     by (simp_all del: replicate.simps)
+     by (simp add: m fps_power_nth del: replicate.simps power_Suc)
    also have "\<dots> = (a$0) ^ m"
      unfolding c by (rule setprod_constant, simp)
    finally have ?thesis .}
--- a/src/HOL/NumberTheory/Gauss.thy	Thu Apr 02 13:41:02 2009 +0200
+++ b/src/HOL/NumberTheory/Gauss.thy	Thu Apr 02 13:41:31 2009 +0200
@@ -290,7 +290,7 @@
   using p_prime p_minus_one_l by (auto simp add: A_def zless_zprime_imp_zrelprime)
 
 lemma A_prod_relprime: "zgcd (setprod id A) p = 1"
-  using all_A_relprime finite_A by (simp add: all_relprime_prod_relprime)
+by(rule all_relprime_prod_relprime[OF finite_A all_A_relprime])
 
 
 subsection {* Relationships Between Gauss Sets *}
@@ -416,8 +416,8 @@
   then have one:
     "[setprod id F = setprod (StandardRes p o (op - p)) E] (mod p)"
     apply simp
-    apply (insert p_g_0 finite_E)
-    by (auto simp add: StandardRes_prod)
+    apply (insert p_g_0 finite_E StandardRes_prod)
+    by (auto)
   moreover have a: "\<forall>x \<in> E. [p - x = 0 - x] (mod p)"
     apply clarify
     apply (insert zcong_id [of p])
@@ -435,10 +435,9 @@
   ultimately have c:
     "[setprod (StandardRes p o (op - p)) E = setprod (uminus) E](mod p)"
     apply simp
-    apply (insert finite_E p_g_0)
-    apply (rule setprod_same_function_zcong
-      [of E "StandardRes p o (op - p)" uminus p], auto)
-    done
+    using finite_E p_g_0
+      setprod_same_function_zcong [of E "StandardRes p o (op - p)" uminus p]
+    by auto
   then have two: "[setprod id F = setprod (uminus) E](mod p)"
     apply (insert one c)
     apply (rule zcong_trans [of "setprod id F"
@@ -463,11 +462,11 @@
   "[a ^ nat((p - 1) div 2) = (-1) ^ (card E)] (mod p)"
 proof -
   have "[setprod id A = setprod id F * setprod id D](mod p)"
-    by (auto simp add: prod_D_F_eq_prod_A zmult_commute)
+    by (auto simp add: prod_D_F_eq_prod_A zmult_commute cong del:setprod_cong)
   then have "[setprod id A = ((-1)^(card E) * setprod id E) *
       setprod id D] (mod p)"
     apply (rule zcong_trans)
-    apply (auto simp add: prod_F_zcong zcong_scalar)
+    apply (auto simp add: prod_F_zcong zcong_scalar cong del: setprod_cong)
     done
   then have "[setprod id A = ((-1)^(card E) * setprod id C)] (mod p)"
     apply (rule zcong_trans)
@@ -476,14 +475,14 @@
     done
   then have "[setprod id A = ((-1)^(card E) * setprod id B)] (mod p)"
     apply (rule zcong_trans)
-    apply (simp add: C_B_zcong_prod zcong_scalar2)
+    apply (simp add: C_B_zcong_prod zcong_scalar2 cong del:setprod_cong)
     done
   then have "[setprod id A = ((-1)^(card E) *
     (setprod id ((%x. x * a) ` A)))] (mod p)"
     by (simp add: B_def)
   then have "[setprod id A = ((-1)^(card E) * (setprod (%x. x * a) A))]
     (mod p)"
-    by (simp add:finite_A inj_on_xa_A setprod_reindex_id[symmetric])
+    by (simp add:finite_A inj_on_xa_A setprod_reindex_id[symmetric] cong del:setprod_cong)
   moreover have "setprod (%x. x * a) A =
     setprod (%x. a) A * setprod id A"
     using finite_A by (induct set: finite) auto
@@ -506,7 +505,7 @@
   then have "[setprod id A * (-1)^(card E) = setprod id A *
       a^(card A)](mod p)"
     apply (rule zcong_trans)
-    apply (simp add: aux)
+    apply (simp add: aux cong del:setprod_cong)
     done
   with this zcong_cancel2 [of p "setprod id A" "-1 ^ card E" "a ^ card A"]
       p_g_0 A_prod_relprime have "[-1 ^ card E = a ^ card A](mod p)"
--- a/src/HOL/Tools/atp_manager.ML	Thu Apr 02 13:41:02 2009 +0200
+++ b/src/HOL/Tools/atp_manager.ML	Thu Apr 02 13:41:31 2009 +0200
@@ -85,36 +85,25 @@
 (* state of thread manager *)
 
 datatype T = State of
- {timeout_heap: ThreadHeap.T,
+ {managing_thread: Thread.thread option,
+  timeout_heap: ThreadHeap.T,
   oldest_heap: ThreadHeap.T,
   active: (Thread.thread * (Time.time * Time.time * string)) list,
   cancelling: (Thread.thread * (Time.time * Time.time * string)) list,
   messages: string list,
   store: string list};
 
-fun make_state timeout_heap oldest_heap active cancelling messages store =
-  State {timeout_heap = timeout_heap, oldest_heap = oldest_heap,
+fun make_state managing_thread timeout_heap oldest_heap active cancelling messages store =
+  State {managing_thread = managing_thread, timeout_heap = timeout_heap, oldest_heap = oldest_heap,
     active = active, cancelling = cancelling, messages = messages, store = store};
 
-fun empty_state state =
-  let
-    val State {active = active, cancelling = cancelling, messages = messages, ...} =
-      Synchronized.value state
-  in (null active) andalso (null cancelling) andalso (null messages) end;
-
-val state = Synchronized.var "atp_manager" (make_state ThreadHeap.empty ThreadHeap.empty [] [] [] []);
-
-
-(* the managing thread *)
-
-(*watches over running threads and interrupts them if required*)
-val managing_thread = ref (NONE: Thread.thread option);
-
+val state = Synchronized.var "atp_manager"
+  (make_state NONE ThreadHeap.empty ThreadHeap.empty [] [] [] []);
 
 (* unregister thread *)
 
 fun unregister (success, message) thread = Synchronized.change state
-  (fn state as State {timeout_heap, oldest_heap, active, cancelling, messages, store} =>
+  (fn state as State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
     (case lookup_thread active thread of
       SOME (birthtime, _, description) =>
         let
@@ -132,7 +121,9 @@
           val store' = message' ::
             (if length store <= message_store_limit then store
              else #1 (chop message_store_limit store))
-        in make_state timeout_heap oldest_heap active' cancelling' (message' :: messages) store' end
+        in make_state
+          managing_thread timeout_heap oldest_heap active' cancelling' (message' :: messages) store'
+        end
     | NONE => state));
 
 
@@ -147,12 +138,13 @@
 fun kill_oldest () =
   let exception Unchanged in
     Synchronized.change_result state
-      (fn State {timeout_heap, oldest_heap, active, cancelling, messages, store} =>
+      (fn State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
         if ThreadHeap.is_empty oldest_heap orelse not (excessive_atps active)
         then raise Unchanged
         else
           let val ((_, oldest_thread), oldest_heap') = ThreadHeap.min_elem oldest_heap
-          in (oldest_thread, make_state timeout_heap oldest_heap' active cancelling messages store) end)
+          in (oldest_thread,
+          make_state managing_thread timeout_heap oldest_heap' active cancelling messages store) end)
       |> unregister (false, "Interrupted (maximum number of ATPs exceeded)")
     handle Unchanged => ()
   end;
@@ -167,8 +159,8 @@
 
 fun print_new_messages () =
   let val to_print = Synchronized.change_result state
-    (fn State {timeout_heap, oldest_heap, active, cancelling, messages, store} =>
-      (messages, make_state timeout_heap oldest_heap active cancelling [] store))
+    (fn State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
+      (messages, make_state managing_thread timeout_heap oldest_heap active cancelling [] store))
   in
     if null to_print then ()
     else priority ("Sledgehammer: " ^ space_implode "\n\n" to_print)
@@ -177,55 +169,66 @@
 
 (* start a watching thread -- only one may exist *)
 
-fun check_thread_manager () = CRITICAL (fn () =>
-  if (case ! managing_thread of SOME thread => Thread.isActive thread | NONE => false)
-  then () else managing_thread := SOME (SimpleThread.fork false (fn () =>
-    let
-      val min_wait_time = Time.fromMilliseconds 300
-      val max_wait_time = Time.fromSeconds 10
+fun check_thread_manager () = Synchronized.change state
+  (fn State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
+    if (case managing_thread of SOME thread => Thread.isActive thread | NONE => false)
+    then make_state managing_thread timeout_heap oldest_heap active cancelling messages store
+    else let val managing_thread = SOME (SimpleThread.fork false (fn () =>
+      let
+        val min_wait_time = Time.fromMilliseconds 300
+        val max_wait_time = Time.fromSeconds 10
 
-      (* wait for next thread to cancel, or maximum*)
-      fun time_limit (State {timeout_heap, ...}) =
-        (case try ThreadHeap.min timeout_heap of
-          NONE => SOME (Time.+ (Time.now (), max_wait_time))
-        | SOME (time, _) => SOME time)
+        (* wait for next thread to cancel, or maximum*)
+        fun time_limit (State {timeout_heap, ...}) =
+          (case try ThreadHeap.min timeout_heap of
+            NONE => SOME (Time.+ (Time.now (), max_wait_time))
+          | SOME (time, _) => SOME time)
 
-      (* action: find threads whose timeout is reached, and interrupt cancelling threads *)
-      fun action (State {timeout_heap, oldest_heap, active, cancelling, messages, store}) =
-        let val (timeout_threads, timeout_heap') =
-          ThreadHeap.upto (Time.now (), Thread.self ()) timeout_heap
-        in
-          if null timeout_threads andalso null cancelling andalso not (excessive_atps active)
-          then NONE
-          else
-            let
-              val _ = List.app (SimpleThread.interrupt o #1) cancelling
-              val cancelling' = filter (Thread.isActive o #1) cancelling
-              val state' = make_state timeout_heap' oldest_heap active cancelling' messages store
-            in SOME (map #2 timeout_threads, state') end
-        end
-    in
-      while not (empty_state state) do
-       (Synchronized.timed_access state time_limit action
-        |> these
-        |> List.app (unregister (false, "Interrupted (reached timeout)"));
-        kill_excessive ();
-        print_new_messages ();
-        (*give threads time to respond to interrupt*)
-        OS.Process.sleep min_wait_time)
-    end)));
+        (* action: find threads whose timeout is reached, and interrupt cancelling threads *)
+        fun action (State {managing_thread, timeout_heap, oldest_heap, active, cancelling,
+                           messages, store}) =
+          let val (timeout_threads, timeout_heap') =
+            ThreadHeap.upto (Time.now (), Thread.self ()) timeout_heap
+          in
+            if null timeout_threads andalso null cancelling andalso not (excessive_atps active)
+            then NONE
+            else
+              let
+                val _ = List.app (SimpleThread.interrupt o #1) cancelling
+                val cancelling' = filter (Thread.isActive o #1) cancelling
+                val state' = make_state
+                  managing_thread timeout_heap' oldest_heap active cancelling' messages store
+              in SOME (map #2 timeout_threads, state') end
+          end
+      in
+        while Synchronized.change_result state
+          (fn st as
+            State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
+            if (null active) andalso (null cancelling) andalso (null messages)
+            then (false, make_state NONE timeout_heap oldest_heap active cancelling messages store)
+            else (true, st))
+        do
+          (Synchronized.timed_access state time_limit action
+            |> these
+            |> List.app (unregister (false, "Interrupted (reached timeout)"));
+            kill_excessive ();
+            print_new_messages ();
+            (*give threads time to respond to interrupt*)
+            OS.Process.sleep min_wait_time)
+      end))
+    in make_state managing_thread timeout_heap oldest_heap active cancelling messages store end);
 
 
 (* thread is registered here by sledgehammer *)
 
 fun register birthtime deadtime (thread, desc) =
  (Synchronized.change state
-    (fn State {timeout_heap, oldest_heap, active, cancelling, messages, store} =>
+    (fn State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
       let
         val timeout_heap' = ThreadHeap.insert (deadtime, thread) timeout_heap
         val oldest_heap' = ThreadHeap.insert (birthtime, thread) oldest_heap
         val active' = update_thread (thread, (birthtime, deadtime, desc)) active
-      in make_state timeout_heap' oldest_heap' active' cancelling messages store end);
+      in make_state managing_thread timeout_heap' oldest_heap' active' cancelling messages store end);
   check_thread_manager ());
 
 
@@ -235,9 +238,11 @@
 (* kill: move all threads to cancelling *)
 
 fun kill () = Synchronized.change state
-  (fn State {timeout_heap, oldest_heap, active, cancelling, messages, store} =>
+  (fn State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
     let val formerly_active = map (fn (th, (tb, _, desc)) => (th, (tb, Time.now (), desc))) active
-    in make_state timeout_heap oldest_heap [] (formerly_active @ cancelling) messages store end);
+    in make_state
+      managing_thread timeout_heap oldest_heap [] (formerly_active @ cancelling) messages store
+    end);
 
 
 (* ATP info *)
--- a/src/HOL/Tools/function_package/fundef_common.ML	Thu Apr 02 13:41:02 2009 +0200
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Thu Apr 02 13:41:31 2009 +0200
@@ -246,6 +246,8 @@
                              ("Head symbol of left hand side must be " 
                               ^ plural "" "one out of " fnames ^ commas_quote fnames)
                                             
+            val _ = length args > 0 orelse input_error "Function has no arguments:"
+
             fun add_bvs t is = add_loose_bnos (t, 0, is)
             val rvs = (add_bvs rhs [] \\ fold add_bvs args [])
                         |> map (fst o nth (rev qs))
--- a/src/HOLCF/Tools/domain/domain_theorems.ML	Thu Apr 02 13:41:02 2009 +0200
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Thu Apr 02 13:41:31 2009 +0200
@@ -610,7 +610,7 @@
     |> (snd o PureThy.add_thmss [
         ((Binding.name "iso_rews" , iso_rews  ), [Simplifier.simp_add]),
         ((Binding.name "exhaust"  , [exhaust] ), []),
-        ((Binding.name "casedist" , [casedist]), [Induct.cases_type (Long_Name.base_name dname)]),
+        ((Binding.name "casedist" , [casedist]), [Induct.cases_type dname]),
         ((Binding.name "when_rews", when_rews ), [Simplifier.simp_add]),
         ((Binding.name "compacts", con_compacts), [Simplifier.simp_add]),
         ((Binding.name "con_rews", con_rews), [Simplifier.simp_add]),
@@ -999,6 +999,9 @@
     in pg [] goal (K tacs) end;
 end; (* local *)
 
+val inducts = ProjectRule.projections (ProofContext.init thy) ind;
+fun ind_rule (dname, rule) = ((Binding.empty, [rule]), [Induct.induct_type dname]);
+
 in thy |> Sign.add_path comp_dnam
        |> (snd o (PureThy.add_thmss (map (Thm.no_attributes o apfst Binding.name) [
 		("take_rews"  , take_rews  ),
@@ -1007,6 +1010,7 @@
 		("finite_ind", [finite_ind]),
 		("ind"       , [ind       ]),
 		("coind"     , [coind     ])])))
+       |> (snd o (PureThy.add_thmss (map ind_rule (dnames ~~ inducts))))
        |> Sign.parent_path |> pair take_rews
 end; (* let *)
 end; (* local *)
--- a/src/Pure/README	Thu Apr 02 13:41:02 2009 +0200
+++ b/src/Pure/README	Thu Apr 02 13:41:31 2009 +0200
@@ -15,7 +15,6 @@
 
 Now the Pure session may be compiled interactively as follows:
 
-  isabelle-process -u RAW
+  isabelle tty -l RAW
+  use "ROOT.ML";
 
-See ROOT.ML for further information.
-
--- a/src/Pure/ROOT.ML	Thu Apr 02 13:41:02 2009 +0200
+++ b/src/Pure/ROOT.ML	Thu Apr 02 13:41:31 2009 +0200
@@ -1,7 +1,4 @@
-(*  Title:      Pure/ROOT.ML
-
-Pure Isabelle.
-*)
+(* Pure Isabelle *)
 
 structure Distribution =     (*filled-in by makedist*)
 struct