diff --git a/src/main/antlr4/edu/kit/formal/psdb/termmatcher/MatchPattern.g4 b/src/main/antlr4/edu/kit/formal/psdb/termmatcher/MatchPattern.g4
index 2787bdfcdaef4f826fc89bab8482647ac497f9e0..4804b0f256ca92f11d0d6450b9ca015c06035513 100644
--- a/src/main/antlr4/edu/kit/formal/psdb/termmatcher/MatchPattern.g4
+++ b/src/main/antlr4/edu/kit/formal/psdb/termmatcher/MatchPattern.g4
@@ -34,6 +34,21 @@ STARDONTCARE: '...' | '…';
 DIGITS : DIGIT+ ;
 fragment DIGIT : [0-9] ;
 SID: '?' [_a-zA-Z0-9\\]+ ;
-ID : [a-zA-Z\\_] ([_a-zA-Z0-9\\])* ;
+ID : [a-zA-Z\\_] ([_a-zA-Z0-9\\])*;
+
+
+PLUS : '+' ;
+MINUS : '-' ;
+MUL : '*' ;
+DIV : '/' ;
+EQ : '=' ;
+NEQ : '!=' ;
+GEQ : '>=' ;
+LEQ : '<=' ;
+GE : '>' ;
+LE : '<' ;
+AND : '&' ;
+OR: '|' ;
+
 COMMENT: '//' ~[\n\r]* -> channel(HIDDEN);
 WS: [\n\f\r\t ] -> channel(HIDDEN);
\ No newline at end of file
diff --git a/src/main/java/edu/kit/formal/psdb/gui/controller/DebuggerMain.java b/src/main/java/edu/kit/formal/psdb/gui/controller/DebuggerMain.java
index 3019e42bb2916e59bbe23aa54f4cc2321a0777a1..37ac72d11c95ac5d0834f08c7574ae237e6d799f 100644
--- a/src/main/java/edu/kit/formal/psdb/gui/controller/DebuggerMain.java
+++ b/src/main/java/edu/kit/formal/psdb/gui/controller/DebuggerMain.java
@@ -771,6 +771,7 @@ public class DebuggerMain implements Initializable {
         WebEngine webEngine = browser.getEngine();
         webEngine.load(url);
         DockNode dn = new DockNode(browser);
+        dn.setTitle("ScriptLanguage Description");
         //this.dockStation.getChildren().add(dn);
         dn.dock(dockStation, DockPos.LEFT);
     }
diff --git a/src/main/java/edu/kit/formal/psdb/gui/controls/WelcomePane.java b/src/main/java/edu/kit/formal/psdb/gui/controls/WelcomePane.java
index 843f15597aef0f564922d68a0b51d562295496d3..391831740c21beb84392a3285bed0b1e9fb284e8 100644
--- a/src/main/java/edu/kit/formal/psdb/gui/controls/WelcomePane.java
+++ b/src/main/java/edu/kit/formal/psdb/gui/controls/WelcomePane.java
@@ -42,6 +42,7 @@ public class WelcomePane extends AnchorPane {
 
     public void loadHelpPage(ActionEvent event) {
         proofScriptDebugger.getWelcomePaneDock().close();
+        proofScriptDebugger.showCommandHelp(event);
         proofScriptDebugger.showHelpText();
 
 
diff --git a/src/main/resources/edu/kit/formal/psdb/gui/intro.html b/src/main/resources/edu/kit/formal/psdb/gui/intro.html
index 32610e9c14011481a692ee4a4d0240eba92b24a5..6a231bcd66d871edf1490fa759a846990ad28f39 100644
--- a/src/main/resources/edu/kit/formal/psdb/gui/intro.html
+++ b/src/main/resources/edu/kit/formal/psdb/gui/intro.html
@@ -77,7 +77,11 @@ inst_occ="...").
 
 </ul>
 <h3>Macro-Commands</h3>
-
+In the KeY system macro commands are proof strategies tailored to specific proof tasks.
+The available macro commands are listed below. Using them in a script is similar to using rule commands:
+<br>
+MACRONAME (PARAMETERS)?
+<br>
 <!--
 
 
diff --git a/src/test/java/edu/kit/formal/psdb/termmatcher/MatcherFacadeTest.java b/src/test/java/edu/kit/formal/psdb/termmatcher/MatcherFacadeTest.java
index ec74942ee97bba477d796dc07b0a4400f4c8e8fc..9c399e82b777bf5bd606413440e71298b94a957d 100644
--- a/src/test/java/edu/kit/formal/psdb/termmatcher/MatcherFacadeTest.java
+++ b/src/test/java/edu/kit/formal/psdb/termmatcher/MatcherFacadeTest.java
@@ -41,7 +41,9 @@ public class MatcherFacadeTest {
         shouldMatch("h(a,b)", "h(?X,?X)", "[]");
         shouldMatch("f(a)", "f(a)");
         shouldMatchForm("pred(a)", "_");
-        shouldMatchForm("pred(a)", "pred(?X)", "[{?X=a}]");
+        shouldMatchForm("pred(a)", "...?X...", "[{?X=pred(a)}, {?X=a}]");
+        shouldMatchForm("pred(f(a))", "pred(...?X...)", "[{?X=f(a)}, {?X=a}]");
+        shouldMatch("i+j", "add(?X,?Y)", "[{?X=i, ?Y=j}]");
 
 
         //shouldMatch("f(a) ==> f(a), f(b)" , "==> f(?X)", [{?X=a}]);
@@ -117,11 +119,14 @@ public class MatcherFacadeTest {
         shouldMatchSemiSeq("pred(a), pred(b) ==>", "pred(?X), pred(?X)", "[]");
         shouldMatchSemiSeq("pred(a), pred(f(a)) ==>", "pred(?X), pred(f(?X))", "[{?X=a}]");
         shouldMatchSemiSeq("pred(b), pred(f(a)) ==>", "pred(?X), pred(f(?X))", "[]");
-
-
         shouldMatchSemiSeq("pred(a), pred(b) ==> qpred(a,b)", "pred(a), pred(b)");
         shouldMatchSemiSeq("pred(a), pred(b) ==> qpred(a,b)", "pred(?X), pred(?Y)", "[{?X=a, ?Y=b}, {?X=b, ?Y=a}]");
 
+        shouldMatchSemiSeq("pred(b), pred(a) ==>", "pred(...?X...), pred(f(?X))", "[]");
+        shouldMatchSemiSeq("pred(b), pred(a) ==>", "pred(...?X...), pred(...?Y...)", "[{?X=b, ?Y=a}, {?X=a, ?Y=b}]");
+
+        shouldMatchSemiSeq("intPred(fint(i+j))", "intPred(...add(?X, ?y)...)");
+
     }
 
     private void shouldMatchSemiSeq(String s, String s1, String exp) throws ParserException {
@@ -149,7 +154,9 @@ public class MatcherFacadeTest {
         shouldMatchSeq("pred(a), pred(b) ==> pred(b)", "pred(?X), pred(?Z) ==> pred(?X)", "[{?X=b, ?Z=a}]");
         shouldMatchSeq("pred(a), pred(b) ==> pred(b)", "pred(?X), pred(?Z) ==>", "[{?X=a, ?Z=b}, {?X=b, ?Z=a}]");
         shouldMatchSeq("pred(f(a)), pred(b) ==> pred(b)", "pred(?X), pred(?Z) ==>", "[{?X=f(a), ?Z=b}, {?X=b, ?Z=f(a)}]");
-
+        shouldMatchSeq("pred(f(a)), pred(b) ==> pred(b)", "pred(...?X...) ==>", "[{?X=f(a)}, {?X=a}, {?X=b}]");
+        shouldMatchSeq("==> pred(a)", "==>", "[{EMPTY_MATCH=null}]");
+        shouldMatchSeq("pred(a) ==> ", "==>", "[{EMPTY_MATCH=null}]");
 
     }
 
diff --git a/src/test/resources/edu/kit/formal/psdb/termmatcher/test.key b/src/test/resources/edu/kit/formal/psdb/termmatcher/test.key
index b13ff383383de420a277796a81e9fb66f3927dd8..0112ddff7e37bc6b97d4e893bafab4e19d2eb0a1 100644
--- a/src/test/resources/edu/kit/formal/psdb/termmatcher/test.key
+++ b/src/test/resources/edu/kit/formal/psdb/termmatcher/test.key
@@ -18,10 +18,12 @@
 
 \functions {
    S a; S b; S c;
-
+   int i; int j;
    S f(S);
    S g(S);
    S h(S, S);
+
+   int fint(int);
 }
 
 \predicates {
@@ -29,6 +31,7 @@
 	q;
 	pred(S);
 	qpred(S, S);
+	intPred(int);
 }
 
 \problem {