--- a/src/HOL/Algebra/UnivPoly.thy Fri May 05 21:59:49 2006 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy Fri May 05 22:11:19 2006 +0200
@@ -297,7 +297,7 @@
then have "k <= n ==>
(\<Oplus>j \<in> {..k}. (\<Oplus>i \<in> {..j}. a i \<otimes> b (j-i)) \<otimes> c (n-j)) =
(\<Oplus>j \<in> {..k}. a j \<otimes> (\<Oplus>i \<in> {..k-j}. b i \<otimes> c (n-j-i)))"
- (concl is "?eq k")
+ (is "_ \<Longrightarrow> ?eq k")
proof (induct k)
case 0 then show ?case by (simp add: Pi_def m_assoc)
next
@@ -344,7 +344,7 @@
then have "k <= n ==>
(\<Oplus>i \<in> {..k}. a i \<otimes> b (n-i)) =
(\<Oplus>i \<in> {..k}. a (k-i) \<otimes> b (i+n-k))"
- (concl is "?eq k")
+ (is "_ \<Longrightarrow> ?eq k")
proof (induct k)
case 0 then show ?case by (simp add: Pi_def)
next
--- a/src/HOL/Library/Multiset.thy Fri May 05 21:59:49 2006 +0200
+++ b/src/HOL/Library/Multiset.thy Fri May 05 22:11:19 2006 +0200
@@ -394,7 +394,7 @@
lemma less_add: "(N, M0 + {#a#}) \<in> mult1 r ==>
(\<exists>M. (M, M0) \<in> mult1 r \<and> N = M + {#a#}) \<or>
(\<exists>K. (\<forall>b. b :# K --> (b, a) \<in> r) \<and> N = M0 + K)"
- (concl is "?case1 (mult1 r) \<or> ?case2")
+ (is "_ \<Longrightarrow> ?case1 (mult1 r) \<or> ?case2")
proof (unfold mult1_def)
let ?r = "\<lambda>K a. \<forall>b. b :# K --> (b, a) \<in> r"
let ?R = "\<lambda>N M. \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and> ?r K a"