src/HOL/BNF/Tools/bnf_comp_tactics.ML

      rtac @{thm Cinfinite_cexp} THEN'
      (rtac ordLeq_csum2 ORELSE' rtac @{thm ordLeq_refl}) THEN'
      rtac Card_order_ctwo THEN'
      (TRY o (rtac @{thm Cinfinite_csum} THEN' rtac disjI1) THEN' rtac (hd Fbd_Cinfs) ORELSE'
        rtac (hd Fbd_Cinfs)) THEN'
-     rtac disjI1 THEN'
-     TRY o rtac csum_Cnotzero2 THEN'
-     rtac ctwo_Cnotzero THEN'
      rtac Gbd_Card_order THEN'
      rtac @{thm cexp_cprod} THEN'
-     TRY o rtac csum_Cnotzero2 THEN'
-     rtac ctwo_Cnotzero) 1
+     rtac @{thm Card_order_csum}) 1
   end;
 
 val comp_wit_thms = @{thms Union_empty_conv o_apply collect_def SUP_def
   Union_image_insert Union_image_empty};
 

     rtac @{thm ordIso_refl} THEN'
     (rtac card_of_Card_order ORELSE' rtac Card_order_csum)) 1
   else all_tac) THEN
   (rtac @{thm csum_com} THEN'
   rtac bd_Card_order THEN'
-  rtac disjI1 THEN'
-  rtac csum_Cnotzero2 THEN'
-  rtac ctwo_Cnotzero THEN'
-  rtac disjI1 THEN'
-  rtac csum_Cnotzero2 THEN'
-  TRY o rtac csum_Cnotzero1 THEN'
-  rtac Cnotzero_UNIV THEN'
   rtac @{thm ordLeq_ordIso_trans} THEN'
   rtac @{thm cexp_mono1} THEN'
   rtac ctrans THEN'
   rtac @{thm csum_mono2} THEN'
   rtac @{thm ordLeq_cprod1} THEN'

   rtac Cnotzero_UNIV THEN'
   rtac bd_Cinfinite THEN'
   ((rtac Card_order_ctwo THEN' rtac @{thm ordLeq_refl}) ORELSE'
     (rtac Card_order_csum THEN' rtac ordLeq_csum2)) THEN'
   rtac Card_order_ctwo THEN'
-  rtac disjI1 THEN'
-  rtac csum_Cnotzero2 THEN'
-  TRY o rtac csum_Cnotzero1 THEN'
-  rtac Cnotzero_UNIV THEN'
   rtac bd_Card_order THEN'
   rtac @{thm cexp_cprod_ordLeq} THEN'
-  TRY o rtac csum_Cnotzero2 THEN'
-  rtac ctwo_Cnotzero THEN'
+  resolve_tac @{thms Card_order_csum Card_order_ctwo} THEN'
   rtac @{thm Cinfinite_cprod2} THEN'
   TRY o rtac csum_Cnotzero1 THEN'
   rtac Cnotzero_UNIV THEN'
   rtac bd_Cinfinite THEN'
   rtac bd_Cnotzero THEN'

     rtac ordLeq_csum2 THEN'
     (rtac Card_order_csum ORELSE' rtac card_of_Card_order)) 1) THEN
   (rtac ordLeq_csum2 THEN'
   (rtac Card_order_csum ORELSE' rtac card_of_Card_order)) 1) ORELSE
   (rtac ordLeq_csum2 THEN' rtac Card_order_ctwo) 1) THEN
-  (rtac disjI1 THEN' TRY o rtac csum_Cnotzero2 THEN' rtac ctwo_Cnotzero
-   THEN' rtac bd_Card_order) 1;
+  (rtac bd_Card_order) 1;
 
 
 
 (* Permute operation *)
 

   mk_rotate_eq_tac
     (rtac @{thm ordIso_refl} THEN'
       FIRST' [rtac card_of_Card_order, rtac Card_order_csum])
     ordIso_transitive @{thm csum_assoc} @{thm csum_com} @{thm csum_cong}
     src dest THEN'
-  rtac bd_Card_order THEN'
-  rtac disjI1 THEN'
-  TRY o rtac csum_Cnotzero2 THEN'
-  rtac ctwo_Cnotzero THEN'
-  rtac disjI1 THEN'
-  TRY o rtac csum_Cnotzero2 THEN'
-  rtac ctwo_Cnotzero) 1;
+  rtac bd_Card_order) 1;
 
 fun mk_map_wpull_tac comp_in_alt inner_map_wpulls outer_map_wpull =
   (rtac (@{thm wpull_cong} OF (replicate 3 comp_in_alt)) THEN' rtac outer_map_wpull) 1 THEN
   WRAP (fn thm => rtac thm 1 THEN REPEAT_DETERM (atac 1)) (K all_tac) inner_map_wpulls all_tac THEN
   TRY (REPEAT_DETERM (atac 1 ORELSE rtac @{thm wpull_id} 1));