src/HOL/Decision_Procs/Cooper.thy
 changeset 49962 a8cc904a6820 parent 48891 c0eafbd55de3 child 50252 4aa34bd43228
1.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Fri Oct 19 10:46:42 2012 +0200
1.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Fri Oct 19 15:12:52 2012 +0200
1.3 @@ -413,7 +413,7 @@
1.4  apply (case_tac "c1+c2 = 0",case_tac "n1 \<le> n2", simp_all)
1.5   apply (case_tac "n1 = n2")
1.6    apply(simp_all add: algebra_simps)
1.7 -apply(simp add: left_distrib[symmetric])
1.8 +apply(simp add: distrib_right[symmetric])
1.9  done
1.11  lemma numadd_nb: "\<lbrakk> numbound0 t ; numbound0 s\<rbrakk> \<Longrightarrow> numbound0 (numadd (t,s))"
1.12 @@ -727,7 +727,7 @@
1.13        by (simp add: Let_def split_def)
1.14      from abj 3 m0 have th2: "(?I x (CN 0 ?j ?b) = ?I x a) \<and> ?N ?b" by blast
1.15      from th have "?I x (CN 0 n a') = ?I x (CN 0 (i+?j) ?b)" by simp
1.16 -    also from th2 have "\<dots> = ?I x (CN 0 i (CN 0 ?j ?b))" by (simp add: left_distrib)
1.17 +    also from th2 have "\<dots> = ?I x (CN 0 i (CN 0 ?j ?b))" by (simp add: distrib_right)
1.18    finally have "?I x (CN 0 n a') = ?I  x (CN 0 i a)" using th2 by simp
1.19    with th2 th have ?case using m0 by blast}
1.20  ultimately show ?case by blast
1.21 @@ -754,7 +754,7 @@
1.22    with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
1.23    from abjs 5 have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast
1.24    from th3[simplified] th2[simplified] th[simplified] show ?case
1.25 -    by (simp add: left_distrib)
1.26 +    by (simp add: distrib_right)
1.27  next
1.28    case (6 s t n a)
1.29    let ?ns = "fst (zsplit0 s)"
1.30 @@ -779,7 +779,7 @@
1.31      by (simp add: Let_def split_def)
1.32    from abj 7 have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
1.33    hence "?I x (Mul i t) = i * ?I x (CN 0 ?nt ?at)" by simp
1.34 -  also have "\<dots> = ?I x (CN 0 (i*?nt) (Mul i ?at))" by (simp add: right_distrib)
1.35 +  also have "\<dots> = ?I x (CN 0 (i*?nt) (Mul i ?at))" by (simp add: distrib_left)
1.36    finally show ?case using th th2 by simp
1.37  qed