src/HOL/Induct/Sigma_Algebra.thy

 text \<open>
   This is just a tiny example demonstrating the use of inductive
   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
   of any \<open>\<sigma>\<close>-algebra, merely using the introduction rules, but
   no induction nor cases.