author wenzelm Fri May 05 22:11:19 2006 +0200 (2006-05-05) changeset 19582 a669c98b9c24 parent 19581 4ae6a14b742f child 19583 c5fa77b03442
get rid of 'concl is';
 src/HOL/Algebra/UnivPoly.thy file | annotate | diff | revisions src/HOL/Library/Multiset.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Algebra/UnivPoly.thy	Fri May 05 21:59:49 2006 +0200
1.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Fri May 05 22:11:19 2006 +0200
1.3 @@ -297,7 +297,7 @@
1.4      then have "k <= n ==>
1.5        (\<Oplus>j \<in> {..k}. (\<Oplus>i \<in> {..j}. a i \<otimes> b (j-i)) \<otimes> c (n-j)) =
1.6        (\<Oplus>j \<in> {..k}. a j \<otimes> (\<Oplus>i \<in> {..k-j}. b i \<otimes> c (n-j-i)))"
1.7 -      (concl is "?eq k")
1.8 +      (is "_ \<Longrightarrow> ?eq k")
1.9      proof (induct k)
1.10        case 0 then show ?case by (simp add: Pi_def m_assoc)
1.11      next
1.12 @@ -344,7 +344,7 @@
1.13      then have "k <= n ==>
1.14        (\<Oplus>i \<in> {..k}. a i \<otimes> b (n-i)) =
1.15        (\<Oplus>i \<in> {..k}. a (k-i) \<otimes> b (i+n-k))"
1.16 -      (concl is "?eq k")
1.17 +      (is "_ \<Longrightarrow> ?eq k")
1.18      proof (induct k)
1.19        case 0 then show ?case by (simp add: Pi_def)
1.20      next
```
```     2.1 --- a/src/HOL/Library/Multiset.thy	Fri May 05 21:59:49 2006 +0200
2.2 +++ b/src/HOL/Library/Multiset.thy	Fri May 05 22:11:19 2006 +0200
2.3 @@ -394,7 +394,7 @@
2.4  lemma less_add: "(N, M0 + {#a#}) \<in> mult1 r ==>
2.5      (\<exists>M. (M, M0) \<in> mult1 r \<and> N = M + {#a#}) \<or>
2.6      (\<exists>K. (\<forall>b. b :# K --> (b, a) \<in> r) \<and> N = M0 + K)"
2.7 -  (concl is "?case1 (mult1 r) \<or> ?case2")
2.8 +  (is "_ \<Longrightarrow> ?case1 (mult1 r) \<or> ?case2")
2.9  proof (unfold mult1_def)
2.10    let ?r = "\<lambda>K a. \<forall>b. b :# K --> (b, a) \<in> r"
2.11    let ?R = "\<lambda>N M. \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and> ?r K a"
```