src/ZF/Induct/Multiset.ML

 by (rotate_simp_tac "M:?u" 1);
 by (rotate_simp_tac "M:?u" 2);
 by (rotate_simp_tac "ALL a:A. ?u(a)" 1);
 by (subgoal_tac "setsum(%x. $# mcount(M, x), A)=$# succ(x)" 1);
 by (dtac setsum_succD 1 THEN Auto_tac);
-by (case_tac "1 <M`xa" 1);
+by (case_tac "1 <M`a" 1);
 by (dtac not_lt_imp_le 2);
 by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [nat_le_1_cases])));
-by (subgoal_tac "M=(M(xa:=M`xa #- 1))(xa:=(M(xa:=M`xa #- 1))`xa #+ 1)" 1);
+by (subgoal_tac "M=(M(a:=M`a #- 1))(a:=(M(a:=M`a #- 1))`a #+ 1)" 1);
 by (res_inst_tac [("A","A"),("B","%x. nat"),("D","%x. nat")] fun_extension 2);
 by (REPEAT(rtac update_type 3));
 by (ALLGOALS(Asm_simp_tac));
 by (Clarify_tac 2);
 by (rtac (succ_pred_eq_self RS sym) 2);

 by (rtac subst 1 THEN rtac sym 1 THEN Blast_tac 1 THEN resolve_tac prems 1);
 by (simp_tac (simpset() addsimps [multiset_def, multiset_fun_iff]) 1);
 by (res_inst_tac [("x", "A")] exI 1);
 by (force_tac (claset() addIs [update_type], simpset()) 1);
 by (asm_simp_tac (simpset() addsimps [mset_of_def, mcount_def]) 1);
-by (dres_inst_tac [("x", "M(xa := M ` xa #- 1)")] spec 1);
+by (dres_inst_tac [("x", "M(a := M ` a #- 1)")] spec 1);
 by (dtac mp 1 THEN dtac mp 2);
 by (ALLGOALS(Asm_full_simp_tac));
 by (res_inst_tac [("x", "A")] exI 1);
 by (auto_tac (claset() addIs [update_type], simpset()));
-by (subgoal_tac "Finite({x:cons(xa, A). x~=xa-->0<M`x})" 1);
+by (subgoal_tac "Finite({x:cons(a, A). x~=a-->0<M`x})" 1);
 by (blast_tac(claset() addIs [Collect_subset RS subset_Finite,Finite_cons])2);
-by (dres_inst_tac [("A", "{x:cons(xa, A). x~=xa-->0<M`x}")] setsum_decr 1);
+by (dres_inst_tac [("A", "{x:cons(a, A). x~=a-->0<M`x}")] setsum_decr 1);
 by (dres_inst_tac [("x", "M")] spec 1);
 by (subgoal_tac "multiset(M)" 1);
 by (simp_tac (simpset() addsimps [multiset_def, multiset_fun_iff]) 2);
 by (res_inst_tac [("x", "A")] exI 2);
 by (Force_tac 2);
 by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [mset_of_def])));
 by (dres_inst_tac [("psi", "ALL x:A. ?u(x)")] asm_rl 1);
-by (dres_inst_tac [("x", "xa")] bspec 1);
+by (dres_inst_tac [("x", "a")] bspec 1);
 by (Asm_simp_tac 1);
-by (subgoal_tac "cons(xa, A)= A" 1);
+by (subgoal_tac "cons(a, A)= A" 1);
 by (Blast_tac 2);
-by (rotate_simp_tac "cons(xa, A) = A" 1);
+by (rotate_simp_tac "cons(a, A) = A" 1);
 by (rotate_simp_tac "ALL x:A. ?u(x)" 1);
 by (rotate_simp_tac "ALL x:A. ?u(x)" 2);
-by (subgoal_tac "M=cons(<xa, M`xa>, restrict(M, A-{xa}))" 1);
+by (subgoal_tac "M=cons(<a, M`a>, restrict(M, A-{a}))" 1);
 by (rtac  fun_cons_restrict_eq 2);
-by (subgoal_tac "cons(xa, A-{xa}) = A" 2);
+by (subgoal_tac "cons(a, A-{a}) = A" 2);
 by (REPEAT(Force_tac 2));
-by (res_inst_tac [("a", "cons(<xa, 1>, restrict(M, A - {xa}))")] ssubst 1);
+by (res_inst_tac [("a", "cons(<a, 1>, restrict(M, A - {a}))")] ssubst 1);
 by (Asm_full_simp_tac 1);
-by (subgoal_tac "multiset(restrict(M, A - {xa}))" 1);
+by (subgoal_tac "multiset(restrict(M, A - {a}))" 1);
 by (simp_tac (simpset() addsimps [multiset_def, multiset_fun_iff]) 2);
-by (res_inst_tac [("x", "A-{xa}")] exI 2);
+by (res_inst_tac [("x", "A-{a}")] exI 2);
 by Safe_tac;
-by (res_inst_tac [("A", "A-{xa}")] apply_type 3);
+by (res_inst_tac [("A", "A-{a}")] apply_type 3);
 by (asm_simp_tac (simpset() addsimps [restrict]) 5);
 by (REPEAT(blast_tac (claset() addIs [Finite_Diff, restrict_type]) 2));;
 by (resolve_tac prems 1);
 by (assume_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [mset_of_def]) 1);
-by (dres_inst_tac [("x", "restrict(M, A-{xa})")] spec 1);
+by (dres_inst_tac [("x", "restrict(M, A-{a})")] spec 1);
 by (dtac mp 1);
-by (res_inst_tac [("x", "A-{xa}")] exI 1);
+by (res_inst_tac [("x", "A-{a}")] exI 1);
 by (auto_tac (claset() addIs [Finite_Diff, restrict_type], 
              simpset() addsimps [restrict]));
-by (forw_inst_tac [("A", "A"), ("M", "M"), ("a", "xa")] setsum_decr3 1);
+by (forw_inst_tac [("A", "A"), ("M", "M"), ("a", "a")] setsum_decr3 1);
 by (asm_simp_tac  (simpset() addsimps [multiset_def, multiset_fun_iff]) 1);
 by (Blast_tac 1);
 by (asm_simp_tac (simpset() addsimps [mset_of_def]) 1);
 by (dres_inst_tac [("b", "if ?u then ?v else ?w")] sym 1);
 by (ALLGOALS(rotate_simp_tac "ALL x:A. ?u(x)"));
-by (subgoal_tac "{x:A - {xa} . 0 < restrict(M, A - {x}) ` x} = A - {xa}" 1);
+by (subgoal_tac "{x:A - {a} . 0 < restrict(M, A - {x}) ` x} = A - {a}" 1);
 by (auto_tac (claset() addSIs [setsum_cong], 
               simpset() addsimps [zdiff_eq_iff, 
                zadd_commute, multiset_def, multiset_fun_iff,mset_of_def]));
 qed "multiset_induct_aux";
 

 by (ALLGOALS(asm_full_simp_tac(simpset() 
     addsimps [Un_subset_iff, multiset_on_def])));
 by (res_inst_tac [("x", "x")] bexI 3);
 by (res_inst_tac [("x", "xb")] bexI 3);
 by (Asm_simp_tac 3);
-by (res_inst_tac [("x", "xc")] bexI 3);
+by (res_inst_tac [("x", "K")] bexI 3);
 by (ALLGOALS(asm_simp_tac (simpset() 
     addsimps [FiniteFun_iff_multiset_on, multiset_on_def])));
 by Auto_tac;
 qed "multirel1_mono1";
 

 by (auto_tac (claset(), simpset() addsimps [FiniteFun_iff_multiset_on]));
 by (res_inst_tac [("x", "x")] bexI 1);
 by (res_inst_tac [("x", "xb")] bexI 1);
 by (ALLGOALS(asm_full_simp_tac (simpset() 
     addsimps [FiniteFun_iff_multiset_on, multiset_on_def])));
-by (res_inst_tac [("x", "xc")] bexI 1);
+by (res_inst_tac [("x", "K")] bexI 1);
 by (ALLGOALS(asm_full_simp_tac (simpset() 
     addsimps [FiniteFun_iff_multiset_on,multiset_on_def])));
 by Auto_tac;
 qed "multirel1_mono2";