# HG changeset patch
# User blanchet
# Date 1393847300 -3600
# Node ID a6fa341a6d667c373905bb7fee9fd8587909c9a2
# Parent  3be27c07e36d2291203176e36907bc24b5afecea
life without 'metis'

diff -r 3be27c07e36d -r a6fa341a6d66 src/HOL/BNF_Cardinal_Arithmetic.thy
--- 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)
diff -r 3be27c07e36d -r a6fa341a6d66 src/HOL/BNF_Comp.thy
--- 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"