verus-lang
diff --git a/‎source/vstd/seq.rs‎
Lines changed: 1 addition & 1 deletion b/‎source/vstd/seq.rs‎
Lines changed: 1 addition & 1 deletion
@@ -1786,7 +1786,7 @@ pub broadcast proof fn lemma_seq_add_index2_alt<A>(s1: Seq<A>, s2: Seq<A>, i: in
 
 }
 
-#[deprecated(note = "Seq axioms have been verified, and are now lemmas")]
+#[deprecated(note = "Use `group_seq_lemmas` instead")]
 pub broadcast group group_seq_axioms {
     lemma_seq_index_decreases,
     lemma_seq_subrange_decreases,
Original file line number	Diff line number	Diff line change
`@@ -1786,7 +1786,7 @@ pub broadcast proof fn lemma_seq_add_index2_alt<A>(s1: Seq<A>, s2: Seq<A>, i: in`
`1786`	`1786`
`1787`	`1787`	`}`
`1788`	`1788`
`1789`		`-#[deprecated(note = "Seq axioms have been verified, and are now lemmas")]`
	`1789`	+#[deprecated(note = "Use `group_seq_lemmas` instead")]
`1790`	`1790`	`pub broadcast group group_seq_axioms {`
`1791`	`1791`	`lemma_seq_index_decreases,`
`1792`	`1792`	`lemma_seq_subrange_decreases,`