src/HOL/Finite.ML

 val lemma = result();
 
 Goal "(A,m): cardR ==> (ALL n. (A,n) : cardR --> n=m)";
 by (etac cardR.induct 1);
  by (safe_tac (claset() addSEs [cardR_insertE]));
-by (rename_tac "B b m" 1);
-by (case_tac "a = b" 1);
+by (rename_tac "B b m" 1 THEN case_tac "a = b" 1);
  by (subgoal_tac "A = B" 1);
   by (blast_tac (claset() addEs [equalityE]) 2);
  by (Blast_tac 1);
 by (subgoal_tac "EX C. A = insert b C & B = insert a C" 1);
  by (res_inst_tac [("x","A Int B")] exI 2);

 (*force simplification of "card A < card (insert ...)"*)
 by (etac rev_mp 1);
 by (asm_simp_tac (simpset() addsimps [less_Suc_eq_le]) 1);
 by (rtac impI 1);
 (** LEVEL 10 **)
-by (rename_tac "Aa xa ya Ab xb yb" 1);
- by (case_tac "xa=xb" 1);
+by (rename_tac "Aa xa ya Ab xb yb" 1 THEN case_tac "xa=xb" 1);
  by (subgoal_tac "Aa = Ab" 1);
  by (blast_tac (claset() addSEs [equalityE]) 2);
  by (Blast_tac 1);
 (*case xa ~= xb*)
 by (subgoal_tac "Aa-{xb} = Ab-{xa} & xb : Aa & xa : Ab" 1);