get rid of 'concl is';
authorwenzelm
Fri May 05 22:11:19 2006 +0200 (2006-05-05)
changeset 19582a669c98b9c24
parent 19581 4ae6a14b742f
child 19583 c5fa77b03442
get rid of 'concl is';
src/HOL/Algebra/UnivPoly.thy
src/HOL/Library/Multiset.thy
     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"