diff --git a/de.prob2.disprover.feature/feature.xml b/de.prob2.disprover.feature/feature.xml
index 0f68dfa27b6ca543808573b901f928b00c5e53f6..0985ab4131d530b9831eb8b21ed273c2ac6d541a 100644
--- a/de.prob2.disprover.feature/feature.xml
+++ b/de.prob2.disprover.feature/feature.xml
@@ -7,7 +7,9 @@
       plugin="de.prob.eventb.disprover.ui">
 
    <description url="https://prob.hhu.de/w/">
-      ProB is an animator and model checker for the B-Method. It allows
+Allows using ProB as a (dis)prover while proving POs.
+
+ProB is an animator and model checker for the B-Method. It allows
 fully automatic animation of many B specifications, and can be
 used to systematically check a specification for errors.
 Part of the research and development was conducted within the
diff --git a/de.prob2.feature/feature.xml b/de.prob2.feature/feature.xml
index be05f985d584f8965731f7abf3e33d9771dd242d..10adbd4bdf2cf52b84b9adc6d734ce6984c15263 100644
--- a/de.prob2.feature/feature.xml
+++ b/de.prob2.feature/feature.xml
@@ -7,7 +7,9 @@
       plugin="de.prob.ui">
 
    <description url="https://prob.hhu.de/w/">
-      ProB is an animator and model checker for the B-Method. It allows
+ProB animator plug-in for Rodin. Also includes BMotion Studio.
+
+ProB is an animator and model checker for the B-Method. It allows
 fully automatic animation of many B specifications, and can be
 used to systematically check a specification for errors.
 Part of the research and development was conducted within the
diff --git a/de.prob2.symbolic.feature/feature.xml b/de.prob2.symbolic.feature/feature.xml
index b4894c5b6639a398a102a1fa879043f4aeea4f5f..224b032c48c96230848f9892f2d5f89fbbef0cc9 100644
--- a/de.prob2.symbolic.feature/feature.xml
+++ b/de.prob2.symbolic.feature/feature.xml
@@ -7,7 +7,10 @@
       plugin="de.prob.symbolic">
 
    <description url="https://prob.hhu.de/w/">
-      ProB is an animator and model checker for the B-Method. It allows
+Allows marking constants as symbolic so that the ProB animator will not
+evaluate them eagerly.
+
+ProB is an animator and model checker for the B-Method. It allows
 fully automatic animation of many B specifications, and can be
 used to systematically check a specification for errors.
 Part of the research and development was conducted within the