# HG changeset patch
# User wenzelm
# Date 1146859879 -7200
# Node ID a669c98b9c24ff27c88c01d09680f420a6e1a642
# Parent  4ae6a14b742f1f01486dcc1a2b2c8ad1511d09fd
get rid of 'concl is';

diff -r 4ae6a14b742f -r a669c98b9c24 src/HOL/Algebra/UnivPoly.thy
--- 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
diff -r 4ae6a14b742f -r a669c98b9c24 src/HOL/Library/Multiset.thy
--- 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"