--- a/src/HOL/Induct/Common_Patterns.thy Mon Jun 06 10:34:56 2016 +0200
+++ b/src/HOL/Induct/Common_Patterns.thy Mon Jun 06 11:50:13 2016 +0200
@@ -287,7 +287,7 @@
inductive Even :: "nat \<Rightarrow> bool" where
zero: "Even 0"
-| double: "Even n \<Longrightarrow> Even (2 * n)"
+| double: "Even (2 * n)" if "Even n" for n
lemma
assumes "Even n"
@@ -349,8 +349,8 @@
inductive Evn :: "nat \<Rightarrow> bool" and Odd :: "nat \<Rightarrow> bool"
where
zero: "Evn 0"
-| succ_Evn: "Evn n \<Longrightarrow> Odd (Suc n)"
-| succ_Odd: "Odd n \<Longrightarrow> Evn (Suc n)"
+| succ_Evn: "Odd (Suc n)" if "Evn n" for n
+| succ_Odd: "Evn (Suc n)" if "Odd n" for n
lemma
"Evn n \<Longrightarrow> P1 n"
@@ -384,8 +384,8 @@
inductive star :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" for r
where
- refl: "star r x x"
-| step: "r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"
+ refl: "star r x x" for x
+| step: "star r x z" if "r x y" and "star r y z" for x y z
text \<open>Underscores are replaced by the default name hyps:\<close>
--- a/src/HOL/Induct/Sigma_Algebra.thy Mon Jun 06 10:34:56 2016 +0200
+++ b/src/HOL/Induct/Sigma_Algebra.thy Mon Jun 06 11:50:13 2016 +0200
@@ -13,13 +13,12 @@
definitions in classical mathematics. We define the least \<open>\<sigma>\<close>-algebra over a given set of sets.
\<close>
-inductive_set \<sigma>_algebra :: "'a set set \<Rightarrow> 'a set set"
- for A :: "'a set set"
+inductive_set \<sigma>_algebra :: "'a set set \<Rightarrow> 'a set set" for A :: "'a set set"
where
- basic: "a \<in> \<sigma>_algebra A" if "a \<in> A"
+ basic: "a \<in> \<sigma>_algebra A" if "a \<in> A" for a
| UNIV: "UNIV \<in> \<sigma>_algebra A"
-| complement: "- a \<in> \<sigma>_algebra A" if "a \<in> \<sigma>_algebra A"
-| Union: "(\<Union>i. a i) \<in> \<sigma>_algebra A" if "\<And>i::nat. a i \<in> \<sigma>_algebra A"
+| complement: "- a \<in> \<sigma>_algebra A" if "a \<in> \<sigma>_algebra A" for a
+| Union: "(\<Union>i. a i) \<in> \<sigma>_algebra A" if "\<And>i::nat. a i \<in> \<sigma>_algebra A" for a
text \<open>
The following basic facts are consequences of the closure properties