src/ZF/Induct/Multiset.thy

       \<exists>a \<in> A. \<exists>M0 \<in> Mult(A). \<exists>K \<in> Mult(A).
       N=M0 +# {#a#} & M=M0 +# K & (\<forall>b \<in> mset_of(K). <b,a> \<in> r)}"
 
 definition
   multirel :: "[i, i] => i"  where
-  "multirel(A, r) == multirel1(A, r)^+"                 
+  "multirel(A, r) == multirel1(A, r)^+"
 
   (* ordinal multiset orderings *)
 
 definition
   omultiset :: "i => o"  where

 
 lemma nat_add_eq_1_cases: "[| m \<in> nat; n \<in> nat |] ==> (m #+ n = 1) \<longleftrightarrow> (m=1 & n=0) | (m=0 & n=1)"
 by (induct_tac n) auto
 
 lemma munion_is_single:
-     "[|multiset(M); multiset(N)|] 
+     "[|multiset(M); multiset(N)|]
       ==> (M +# N = {#a#}) \<longleftrightarrow>  (M={#a#} & N=0) | (M = 0 & N = {#a#})"
 apply (simp (no_asm_simp) add: multiset_equality)
 apply safe
 apply simp_all
 apply (case_tac "aa=a")

 apply (rule_tac x = K in bexI)
 apply (auto simp add: Mult_iff_multiset)
 done
 
 lemma multirel1_mono2: "r\<subseteq>s ==> multirel1(A,r)\<subseteq>multirel1(A, s)"
-apply (simp add: multirel1_def, auto) 
+apply (simp add: multirel1_def, auto)
 apply (rule_tac x = a in bexI)
 apply (rule_tac x = M0 in bexI)
 apply (simp_all add: Mult_iff_multiset)
 apply (rule_tac x = K in bexI)
 apply (simp_all add: Mult_iff_multiset, auto)

 apply (auto simp add: Mult_iff_multiset)
 apply (erule_tac P = "\<forall>x \<in> mset_of (K) . <x, a> \<in> r" in rev_mp)
 apply (erule_tac P = "mset_of (K) \<subseteq>A" in rev_mp)
 apply (erule_tac M = K in multiset_induct)
 (* three subgoals *)
-(* subgoal 1: the induction base case *)
+(* subgoal 1 \<in> the induction base case *)
 apply (simp (no_asm_simp))
-(* subgoal 2: the induction general case *)
+(* subgoal 2 \<in> the induction general case *)
 apply (simp add: Ball_def Un_subset_iff, clarify)
 apply (drule_tac x = aa in spec, simp)
 apply (subgoal_tac "aa \<in> A")
 prefer 2 apply blast
 apply (drule_tac x = "M0 +# M" and P =
        "%x. x \<in> acc(multirel1(A, r)) \<longrightarrow> ?Q(x)" in spec)
 apply (simp add: munion_assoc [symmetric])
-(* subgoal 3: additional conditions *)
+(* subgoal 3 \<in> additional conditions *)
 apply (auto intro!: multirel1_base [THEN fieldI2] simp add: Mult_iff_multiset)
 done
 
 lemma lemma2: "[| \<forall>b \<in> A. <b,a> \<in> r
    \<longrightarrow> (\<forall>M \<in> acc(multirel1(A, r)). M +# {#b#} :acc(multirel1(A, r)));