--- a/src/HOL/BNF_Cardinal_Arithmetic.thy Mon Mar 03 12:48:20 2014 +0100
+++ b/src/HOL/BNF_Cardinal_Arithmetic.thy Mon Mar 03 12:48:20 2014 +0100
@@ -351,13 +351,13 @@
by (blast intro: cinfinite_cprod2 Card_order_cprod)
lemma cprod_cong: "\<lbrakk>p1 =o r1; p2 =o r2\<rbrakk> \<Longrightarrow> p1 *c p2 =o r1 *c r2"
-by (metis cprod_mono ordIso_iff_ordLeq)
+unfolding ordIso_iff_ordLeq by (blast intro: cprod_mono)
lemma cprod_cong1: "\<lbrakk>p1 =o r1\<rbrakk> \<Longrightarrow> p1 *c p2 =o r1 *c p2"
-by (metis cprod_mono1 ordIso_iff_ordLeq)
+unfolding ordIso_iff_ordLeq by (blast intro: cprod_mono1)
lemma cprod_cong2: "p2 =o r2 \<Longrightarrow> q *c p2 =o q *c r2"
-by (metis cprod_mono2 ordIso_iff_ordLeq)
+unfolding ordIso_iff_ordLeq by (blast intro: cprod_mono2)
lemma cprod_com: "p1 *c p2 =o p2 *c p1"
by (simp only: cprod_def card_of_Times_commute)
--- a/src/HOL/BNF_Comp.thy Mon Mar 03 12:48:20 2014 +0100
+++ b/src/HOL/BNF_Comp.thy Mon Mar 03 12:48:20 2014 +0100
@@ -134,10 +134,15 @@
unfolding id_bnf_comp_def by unfold_locales auto
lemma csum_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p +c p' =o r +c r \<Longrightarrow> p +c p' =o r"
-by (metis csum_absorb2' ordIso_transitive ordLeq_refl)
+apply (erule ordIso_transitive)
+apply (frule csum_absorb2')
+apply (erule ordLeq_refl)
+by simp
lemma cprod_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p *c p' =o r *c r \<Longrightarrow> p *c p' =o r"
-by (metis cprod_infinite ordIso_transitive)
+apply (erule ordIso_transitive)
+apply (rule cprod_infinite)
+by simp
ML_file "Tools/BNF/bnf_comp_tactics.ML"
ML_file "Tools/BNF/bnf_comp.ML"