# HG changeset patch
# User wenzelm
# Date 1465206613 -7200
# Node ID e53830948c4f5bb20d9d61393b2c2a63fe1a4bb1
# Parent  7238ed9a27ab0183306fc524aef8530f0c0dc39c
tuned;

diff -r 7238ed9a27ab -r e53830948c4f src/HOL/Induct/Common_Patterns.thy
--- 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>
 
diff -r 7238ed9a27ab -r e53830948c4f src/HOL/Induct/Sigma_Algebra.thy
--- 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