diff --git a/src/main/java/edu/kit/formal/interpreter/Interpreter.java b/src/main/java/edu/kit/formal/interpreter/Interpreter.java
index 8be113e1244896600a6ef51a979aff77426063f0..3d09379952558b8585c65e0c95eb09598a43b77a 100644
--- a/src/main/java/edu/kit/formal/interpreter/Interpreter.java
+++ b/src/main/java/edu/kit/formal/interpreter/Interpreter.java
@@ -25,7 +25,7 @@ import java.util.logging.Logger;
  *
  * @author S.Grebing
  */
-public class Interpreter<T> extends DefaultASTVisitor<Void>
+public class Interpreter<T> extends DefaultASTVisitor<Object>
         implements ScopeObservable {
     private static final int MAX_ITERATIONS = 5;
     @Getter
@@ -79,7 +79,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Void>
      * @return
      */
     @Override
-    public Void visit(ProofScript proofScript) {
+    public Object visit(ProofScript proofScript) {
         enterScope(proofScript);
         //add vars
         visit(proofScript.getSignature());
@@ -95,7 +95,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Void>
      * @return
      */
     @Override
-    public Void visit(AssignmentStatement assignmentStatement) {
+    public Object visit(AssignmentStatement assignmentStatement) {
         enterScope(assignmentStatement);
 
         GoalNode<T> node = getSelectedNode();
@@ -152,26 +152,92 @@ public class Interpreter<T> extends DefaultASTVisitor<Void>
         return null;
     }
 
+    @Override
+    public Object visit(IsClosableCase isClosableCase) {
+        State<T> currentStateToMatch = peekState();
+        GoalNode<T> selectedGoal = currentStateToMatch.getSelectedGoalNode();
+        enterScope(isClosableCase);
+        //executebody
+
+        exitScope(isClosableCase);
+        return false;
+    }
+
+    @Override
+    public Object visit(SimpleCaseStatement simpleCaseStatement) {
+        Expression matchExpression = simpleCaseStatement.getGuard();
+        State<T> currentStateToMatch = peekState();
+        GoalNode<T> selectedGoal = currentStateToMatch.getSelectedGoalNode();
+        VariableAssignment va = evaluateMatchInGoal(matchExpression, selectedGoal);
+        if (va != null) {
+            enterScope(simpleCaseStatement);
+            executeBody(simpleCaseStatement.getBody(), selectedGoal, va);
+            //  executeCase(simpleCaseStatement.getBody(), )
+            exitScope(simpleCaseStatement);
+            return true;
+        } else {
+            return false;
+        }
+       /* Map<GoalNode<T>, VariableAssignment> matchedGoals =
+                matchGoal(remainingGoalsSet, (SimpleCaseStatement) aCase);
+        if (matchedGoals != null) {
+            remainingGoalsSet.removeAll(matchedGoals.keySet());
+            goalsAfterCases.addAll(executeCase(aCase.getBody(), matchedGoals));
+        }
+
+        HashMap<GoalNode<T>, VariableAssignment> matchedGoals = new HashMap<>();
+        Expression matchExpression = aCase.getGuard();
+        for (GoalNode<T> goal : allGoalsBeforeCases) {
+            VariableAssignment va = evaluateMatchInGoal(matchExpression, goal);
+            if (va != null) {
+                matchedGoals.put(goal, va);
+            }
+        }
+        return matchedGoals;
+
+        */
+
+    }
+
     /**
      * @param casesStatement
      * @return
      */
     @Override
-    public Void visit(CasesStatement casesStatement) {
+    public Object visit(CasesStatement casesStatement) {
         enterScope(casesStatement);
         State<T> beforeCases = peekState();
 
-
         List<GoalNode<T>> allGoalsBeforeCases = beforeCases.getGoals();
 
         //global List after all Case Statements
         List<GoalNode<T>> goalsAfterCases = new ArrayList<>();
         //copy the list of goal nodes for keeping track of goals
         Set<GoalNode<T>> remainingGoalsSet = new HashSet<>(allGoalsBeforeCases);
-        //TODO
         //handle cases
         List<CaseStatement> cases = casesStatement.getCases();
-        for (CaseStatement aCase : cases) {
+
+        for (GoalNode<T> goalBeforeCase : allGoalsBeforeCases) {
+            State<T> createdState = newState(goalBeforeCase);//to allow the case to retrieve goal
+            for (CaseStatement aCase : cases) {
+                boolean result = (boolean) aCase.accept(this);
+                if (result) {
+                    //remove goal from set for default
+                    remainingGoalsSet.remove(goalBeforeCase);
+                    //case statement matched and was executed
+                    break;
+                }
+            }
+            //remove state from stack
+            State<T> stateAfterCase = popState();
+            if (stateAfterCase.getGoals() != null) {
+                goalsAfterCases.addAll(stateAfterCase.getGoals());
+            }
+
+        }
+
+        //===========================================================================================//
+       /* for (CaseStatement aCase : cases) {
             if (aCase.isClosedStmt) {
                 System.out.println("IsClosableStmt not implemented yet");
             } else {
@@ -183,7 +249,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Void>
                 }
             }
 
-        }
+        }*/
 
         //for all remaining goals execute default
         if (!remainingGoalsSet.isEmpty()) {
@@ -227,14 +293,11 @@ public class Interpreter<T> extends DefaultASTVisitor<Void>
 
         HashMap<GoalNode<T>, VariableAssignment> matchedGoals = new HashMap<>();
         Expression matchExpression = aCase.getGuard();
-
-
         for (GoalNode<T> goal : allGoalsBeforeCases) {
             VariableAssignment va = evaluateMatchInGoal(matchExpression, goal);
             if (va != null) {
                 matchedGoals.put(goal, va);
             }
-
         }
         return matchedGoals;
     }
@@ -244,7 +307,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Void>
      *
      * @param matchExpression
      * @param goal
-     * @return null, if match was false, return teh first Assignment when match was true
+     * @return null, if match was false, return the first Assignment when match was true
      */
     private VariableAssignment evaluateMatchInGoal(Expression matchExpression, GoalNode<T> goal) {
         enterScope(matchExpression);
@@ -308,16 +371,6 @@ public class Interpreter<T> extends DefaultASTVisitor<Void>
         return s;
     }
 
-    /**
-     * @param caseStatement
-     * @return
-     */
-  /*  @Override
-    public Void visit(CaseStatement caseStatement) {
-        enterScope(caseStatement);
-        exitScope(caseStatement);
-        return null;
-    }*/
 
     /**
      * Visiting a call statement results in:
@@ -332,7 +385,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Void>
      * @return
      */
     @Override
-    public Void visit(CallStatement call) {
+    public Object visit(CallStatement call) {
         enterScope(call);
         //neuer VarScope
         //enter new variable scope
@@ -357,7 +410,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Void>
     }
 
     @Override
-    public Void visit(TheOnlyStatement theOnly) {
+    public Object visit(TheOnlyStatement theOnly) {
         List<GoalNode<T>> goals = getCurrentState().getGoals();
         if (goals.size() > 1) {
             throw new IllegalArgumentException(
@@ -381,7 +434,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Void>
      * @return
      */
     @Override
-    public Void visit(ForeachStatement foreach) {
+    public Object visit(ForeachStatement foreach) {
         enterScope(foreach);
         List<GoalNode<T>> allGoals = getCurrentGoals();
         List<GoalNode<T>> goalsAfterForeach = new ArrayList<>();
@@ -399,7 +452,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Void>
     }
 
     @Override
-    public Void visit(RepeatStatement repeatStatement) {
+    public Object visit(RepeatStatement repeatStatement) {
         enterScope(repeatStatement);
         int counter = 0;
         boolean b = false;
@@ -419,7 +472,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Void>
     }
 
     @Override
-    public Void visit(Signature signature) {
+    public Object visit(Signature signature) {
         exitScope(signature);
         GoalNode<T> node = getSelectedNode();
         node.enterScope();
diff --git a/src/main/java/edu/kit/formal/proofscriptparser/TransformAst.java b/src/main/java/edu/kit/formal/proofscriptparser/TransformAst.java
index a86c17f7311c1f7afe108aba682172ab214a78dc..5ebf4d9f8a821d1d54bd3d45cbe97507ef343e83 100644
--- a/src/main/java/edu/kit/formal/proofscriptparser/TransformAst.java
+++ b/src/main/java/edu/kit/formal/proofscriptparser/TransformAst.java
@@ -152,6 +152,11 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
         return createBinaryExpression(ctx, ctx.expression(), findOperator(ctx.op.getText()));
     }
 
+    @Override
+    public Object visitExprSubs(ScriptLanguageParser.ExprSubsContext ctx) {
+        return null;
+    }
+
     private Operator findOperator(String n) {
         return findOperator(n, 2);
     }
@@ -215,6 +220,12 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
 
     }
 
+    //TODO implement
+    @Override
+    public Object visitSubstExpression(ScriptLanguageParser.SubstExpressionContext ctx) {
+        return null;
+    }
+
     @Override
     public Object visitLiteralID(ScriptLanguageParser.LiteralIDContext ctx) {
         return new Variable(ctx.ID().getSymbol());
diff --git a/src/main/resources/edu/kit/formal/gui/intro.html b/src/main/resources/edu/kit/formal/gui/intro.html
index 7cad4490938b4a61e9455e81baeb45ff83e64ac7..c58825490e1c194c1826046314254903aa828a6e 100644
--- a/src/main/resources/edu/kit/formal/gui/intro.html
+++ b/src/main/resources/edu/kit/formal/gui/intro.html
@@ -4,5 +4,260 @@
     <meta content="">
     <style></style>
 </head>
-<body>Test</body>
+<body>
+<h1>Language Constructs</h1>
+<h2>Proof Commands</h2>
+All KeY rules can be used as proof command.
+<!--A rule command has the following syntax:<br>
+RULENAME (on="TERM")? (formula="TOP_LEVEL_FORMULA")? (occ="OCCURENCE_IN_SEQUENT")? (inst_="TERM")?
+<br>with:
+<ul>
+    <li>TERM</li>
+    <li>TOP_LEVEL_FORMULA</li>
+</ul>
+
+FROM MATTIAS:
+Making interactive persistent using proof scripts
+=================================================
+Mattias Ulbrich <ulbrich@kit.edu>, 2015
+
+
+Experimental feature: Proof scripts are currently only visible in the
+GUI if KeY is launched with the --experimental option. Concrete syntax
+is subject to change.
+
+Every KeY user knows the pain of manually redoing an interactive proof
+over and over again even though only a tiny bit of the program or
+specification have changed. NOW you can use proof scripts which will
+alleviate your worries with repeating proofs.
+
+Proof scripts are textual representations of rule applications,
+settings changes and macro invocations. They are notated in linear
+order. The target of a script command is usually the first open goal
+in the proof tree, i.e., the first reached when traversing the proof
+tree (not necessarily the first in the "Goal" pane in the GUI).
+
+
+Syntax of proof scripts
+-----------------------
+
+Proof commands start with an identifier followed by optional
+arguments:
+
+command argName="argument" "argument without name" ;
+
+Every command is terminated with a semicolon. There are named
+arguments in the form argName="argument" and unnamed argument without
+name. Single '...'and double quotes "..." can both be used. If
+"argument" is an identifier itself, the quotes can optionally be
+dropped, like in
+
+rule andRight ;
+
+The character # begins a comment which extends to the end of the
+line. Currently, there are no multi-line comments in proof scripts.
+Proof scripts are case sensitive.
+
+
+How can scripts be loaded
+-------------------------
+
+1. In the GUI:
+
+Open a proof obligation. Currently proof scripts work only reliably if
+applied to the root of a fresh proof obligation (no rule applications,
+prune steps). The open the context menu (sequent or proof tree),
+choose "Strategy macros" and then "Run proof script ...". In the file
+dialog that appears, choose the script file to load. The script is
+automatically applied. You can follow the process in a logging window.
+
+2. From within key input files:
+
+At the very end of key files *INSTEAD* of a \proof object, you can now
+attach a proof script directly in double quotes following the keyword
+\proofScript. An very simple example reads:
+
+----------8<----------
+\predicates {a; b;}
+\problem { a & b -> a }
+
+\proofScript "
+rule 'impRight';
+rule 'andLeft';
+rule 'close';"
+----------8<----------
+
+Since the script is no enclosed in "...", only single quotes '...' can
+be used in the script. You can also load a script from an external
+file by writing
+
+\proofScript "script 'some_filename.script';"
+
+
+Commands in scripts
+-------------------
+
+This list of available script commands is subject to change and to
+extension. If you write your own script commands (s. below), please
+add an explanation to this list here. The list is sorted alphabetically.
+
+-- auto ------------------
+
+Apply the automatic KeY strategy on the current goal. Optinally you
+can specify the number of steps to run.
+
+Examples:
+auto steps=30000;
+# run at most 30000 steps automatically.
+
+-- cut -------------------
+
+Performs a cut and thus splits the sequent into two goals. The unnamed
+argument is the formula to cut with
+
+Examples:
+cut "value1 = value2";
+
+-- exit ------------------
+
+Terminate the script prematurely at that point. Used mainly for debug
+purposes.
+
+Examples:
+exit;
+
+-- instantiate -----------
+
+Quantifier instantiation is a task that often occurs. Instead of
+specifying the entire formula, it suffices here to name the variable
+that is to be instantiated. If that is not unique, the number of the
+occurrence of that quantified variable can be specified as well.
+
+Examples:
+instantiate var="x" occ="3" with="42"
+# Instantiate the third instantiateable formula whose bound
+# variable is called "x" with the value 42
+
+instantiate formula="\forall int x; f(x) = 42" with="23"
+# The quantified formula can also be specified if wanted.
+# This here for the antecedent.
+
+instantiate formula="\exists int x; f(x) = 42" with="23"
+# Existentially quantified variables can be instantiated if they
+# occur on the succedent side.
+
+instantiate hide var=x value="x_0"
+# instantiate x and hide the quantified formula
+
+-- leave -----------------
+
+Mark the currently active goal as non-interactive (the orange hand
+symbol in the GUI). It is then excluded from further analysis by
+scripts. This is good for debugging unfinished proof scripts.
+
+-- macro -----------------
+
+Invoke a macro on the current goal. The names of available macros
+include:
+
+autopilot      full autopilot
+autopilot-prep preparation only autopilot
+split-prop     propositional expansion w/ splits
+nosplit-prop   propositional expansion w/o splits
+simp-upd       update simplification
+simp-heap      heap simplification
+
+Examples:
+macro autopilot-prep;
+
+(Future version may drop the macro keyword and allow macro invocations
+directly.)
+
+-- rule ------------------
+
+Apply a single rule onto the current sequent. As unnamed argument add
+the name of the taclet to be applied. If the taclet matches only once
+on the entire sequent, the rule is applied. If it matches more than
+once you need to specify more. In that case you can first specify the
+sequence formula and then the number of the occurrence in the formula
+or the specific subterm via the 'on' keyword.
+If a rule has schema variables which must be instantiated manually,
+such instantiations can be provided as arguments. A schema variable
+named sv can be instantiated by setting the argument sv="..." or by
+setting inst_sv="..." (the latter works also for conflict cases like
+inst_occ="...").
+
+Examples:
+rule andRight;
+# if there is only one matching spot on the sequent
+
+rule eqSymm formula="a=b";
+# changes sequent "a=b ==> c=d" to "b=a ==> c=d"
+# "rule eqSymm;" alone would have been ambiguous.
+
+rule eqSymm formula="a=b->c=d" occ=2;
+# changes sequent "a=b->c=d ==>" to "a=b->d=c ==>".
+# occurrence number needed since there are
+# two possible applications on the formula
+
+rule eqSymm formula="a=b->c=d" on="c=d";
+# changes sequent "a=b->c=d ==>" to "a=b->d=c ==>".
+# same as above, but using the option to specify a
+# subterm instead of an occurrence number.
+
+rule cut cutFormula="x > y";
+# almost the same as 'cut "x>y"'
+
+-- script ----------------
+
+Invoke another script which resides in an external file.
+
+Example:
+script '/path/to/other/file.script';
+
+-- select ----------------
+
+Unlike most other commands, this command does not change the proof but
+chooses the goal on which the next step operates. Currently you can
+specify a formula. The goal is chosen such that the formula appears
+(toplevel) on the sequent (antecedent or succedent). You can limit the
+search to antecedent or succedent.
+
+Examples:
+select formula="{ x:=1 }y < x";
+# search for the formula anywhere
+select succedent formula="wellFormed(someHeap)";
+# search only the succedent for the formula
+
+-- smt -------------------
+
+Invoke an external SMT solver. That solver must be adequately
+configured outside the script mechanism. By default, Z3 is invoked,
+but that can be chosen.
+
+Examples:
+smt;
+# invoke Z3
+smt solver="Z3,yices";
+# a comma separated list of solvers can be specified.
+
+-- tryclose --------------
+
+Unlike other commands this command operates on ALL open goals and
+effectively applies the "try provable goals below" macro to all of
+them. A number of steps can optionally be given.
+
+Examples:
+tryclose;
+tryclose steps=2000;
+# spend 2000 steps on each open goal
+
+
+Write your on proof commands
+----------------------------
+
+to be done.
+Contact Mattias, if you are interested.
+-->
+</body>
 </html>
\ No newline at end of file