--- a/src/HOL/BNF_Comp.thy Mon Mar 03 03:13:45 2014 +0100
+++ b/src/HOL/BNF_Comp.thy Mon Mar 03 12:48:19 2014 +0100
@@ -128,6 +128,12 @@
end
+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)
+
+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)
+
ML_file "Tools/BNF/bnf_comp_tactics.ML"
ML_file "Tools/BNF/bnf_comp.ML"