--- 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"