diff --git a/key.core/src/main/antlr4/JmlLexer.g4 b/key.core/src/main/antlr4/JmlLexer.g4
index f1a67a2afd5..c6b65084de5 100644
--- a/key.core/src/main/antlr4/JmlLexer.g4
+++ b/key.core/src/main/antlr4/JmlLexer.g4
@@ -82,6 +82,7 @@ CAPTURES: 'captures' Pred -> pushMode(expr);
 CODE: 'code'; //?
 CONSTRAINT: 'constraint' Pred -> pushMode(expr);
 CONTINUES: 'continues' -> pushMode(expr);
+DATATYPE: 'datatype';
 DEBUG: 'debug'; //?
 DECREASING: ('decreasing' | 'decreases' | 'loop_variant') Pred -> pushMode(expr);
 DETERMINES: 'determines' -> pushMode(expr);
@@ -143,6 +144,7 @@ C_IDENT: '\\'? LETTER (LETTERORDIGIT)* -> type(IDENT);
 C_COLON: ':' -> type(COLON);
 C_DOT: '.' -> type(DOT);
 C_COMMA: ',' -> type(COMMA);
+C_INCLUSIVEOR: '|' -> type(INCLUSIVEOR);
 
 SL_COMMENT: {jmlMarkerDecision.isComment("//")}? ('//' ('\n'|'\r'|EOF) | '//' ~'@' ~('\n'|'\r')*) -> channel(HIDDEN);
 ML_COMMENT: {jmlMarkerDecision.isComment("/*")}? '/*' -> more, pushMode(mlComment);
diff --git a/key.core/src/main/antlr4/JmlParser.g4 b/key.core/src/main/antlr4/JmlParser.g4
index a66965df0fd..ff3b91d889f 100644
--- a/key.core/src/main/antlr4/JmlParser.g4
+++ b/key.core/src/main/antlr4/JmlParser.g4
@@ -22,6 +22,7 @@ classlevel_element
   | monitors_for_clause | readable_if_clause | writable_if_clause
   | datagroup_clause    | set_statement      | nowarn_pragma
   | accessible_clause   | assert_statement   | assume_statement
+  | datatype_declaration
   ;
 
 methodlevel_comment: (modifiers? methodlevel_element modifiers?)* EOF;
@@ -41,7 +42,28 @@ modifier
   | CODE_JAVA_MATH | CODE_SAFE_MATH | CODE_BIGINT_MATH)
  ;
 
+datatype_declaration:
+    DATATYPE
+    dt_name=IDENT
+    LBRACE
+    datatype_constructor (INCLUSIVEOR datatype_constructor)*
+    SEMI_TOPLEVEL
+    (datatype_function)*
+    RBRACE
+    ;
+
+datatype_constructor:
+  con_name=IDENT
+  (
+    LPAREN
+    (argType+=type argName+=IDENT
+     (COMMA argType+=type argName+=IDENT)*
+    )?
+    RPAREN
+  )?
+;
 
+datatype_function: type IDENT param_list method_body;
 
 class_axiom: AXIOM expression SEMI_TOPLEVEL;
 initially_clause: INITIALLY expression SEMI_TOPLEVEL;