diff --git a/src/main/java/de/tla2b/analysis/SymbolRenamer.java b/src/main/java/de/tla2b/analysis/SymbolRenamer.java
index 49a2f800aea6e492b2681c9d881d083e09060666..56ed582af98f39e9d4707c83e5d8bfee1e0de17c 100644
--- a/src/main/java/de/tla2b/analysis/SymbolRenamer.java
+++ b/src/main/java/de/tla2b/analysis/SymbolRenamer.java
@@ -110,6 +110,7 @@ public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals,
 		BBUILTIN_OPERATOR.put("\\geq", "geq");
 		BBUILTIN_OPERATOR.put("%", "modulo");
 		BBUILTIN_OPERATOR.put("\\div", "div");
+		BBUILTIN_OPERATOR.put("/", "realdiv");
 		BBUILTIN_OPERATOR.put("..", "dot2");
 	}
 
diff --git a/src/main/java/de/tla2b/analysis/TypeChecker.java b/src/main/java/de/tla2b/analysis/TypeChecker.java
index f51225d3ac5e01a5a41332d8d620bb8988a6b695..3b48ec81c3ce4752cb765e4a0bab59982b34b5aa 100644
--- a/src/main/java/de/tla2b/analysis/TypeChecker.java
+++ b/src/main/java/de/tla2b/analysis/TypeChecker.java
@@ -1229,6 +1229,19 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
 			return type;
 		}
 
+			case B_OPCODE_realdiv: { // /
+				try {
+					RealType.getInstance().unify(expected);
+				} catch (UnificationException e) {
+					throw new TypeErrorException(String.format("Expected %s, found REAL at '%s',%n%s", expected,
+						n.getOperator().getName(), n.getLocation()));
+				}
+				for (int i = 0; i < n.getArgs().length; i++) {
+					visitExprOrOpArgNode(n.getArgs()[i], RealType.getInstance());
+				}
+				return RealType.getInstance();
+			}
+
 		case B_OPCODE_dotdot: // ..
 		{
 			try {
diff --git a/src/main/java/de/tla2b/global/BBuildIns.java b/src/main/java/de/tla2b/global/BBuildIns.java
index af2ca6c81706bf1d80adb0cd2cbe470cf56a6d4d..a36e4257c543a86753a9bfe066c9aa12c49dfd66 100644
--- a/src/main/java/de/tla2b/global/BBuildIns.java
+++ b/src/main/java/de/tla2b/global/BBuildIns.java
@@ -12,6 +12,8 @@ public interface BBuildIns {
 			.uniqueStringOf("*");
 	UniqueString OP_div = UniqueString
 			.uniqueStringOf("\\div");
+	UniqueString OP_realdiv = UniqueString
+		.uniqueStringOf("/");
 	UniqueString OP_mod = UniqueString.uniqueStringOf("%");
 	UniqueString OP_exp = UniqueString.uniqueStringOf("^");
 
@@ -133,4 +135,5 @@ public interface BBuildIns {
 	int B_OPCODE_assert = B_OPCODE_rel_inverse + 1;
 
 	int B_OPCODE_real = B_OPCODE_assert + 1;
+	int B_OPCODE_realdiv = B_OPCODE_real + 1;
 }
diff --git a/src/main/java/de/tla2b/global/BBuiltInOPs.java b/src/main/java/de/tla2b/global/BBuiltInOPs.java
index d1c1d33dae232408575fdcf042ac8fd01918edca..3fdbfd37c54bf278b69145f31540db4732a4253e 100644
--- a/src/main/java/de/tla2b/global/BBuiltInOPs.java
+++ b/src/main/java/de/tla2b/global/BBuiltInOPs.java
@@ -13,6 +13,7 @@ public class BBuiltInOPs implements BBuildIns{
 		B_Opcode_Table.put(OP_minus, B_OPCODE_minus);
 		B_Opcode_Table.put(OP_times, B_OPCODE_times);
 		B_Opcode_Table.put(OP_div, B_OPCODE_div);
+		B_Opcode_Table.put(OP_realdiv, B_OPCODE_realdiv);
 		B_Opcode_Table.put(OP_mod, B_OPCODE_mod);
 		B_Opcode_Table.put(OP_exp, B_OPCODE_exp);
 		B_Opcode_Table.put(OP_uminus, B_OPCODE_uminus);
diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index dfe0e4a12cf543a46c982e4e6694a18a3ec7b231..40317398d2498185668537c9193fb6da0722dc3a 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -1020,6 +1020,15 @@ public class BAstCreator extends BuiltInOPs
 				returnNode = aFlooredDivExpression;
 				break;
 
+			case B_OPCODE_realdiv: // /
+				ADivExpression aDivExpression = new ADivExpression(
+					visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0]),
+					visitExprOrOpArgNodeExpression(opApplNode.getArgs()[1]));
+
+				setPosition(aDivExpression, opApplNode);
+				returnNode = aDivExpression;
+				break;
+
 			case B_OPCODE_dotdot: // ..
 				returnNode = new AIntervalExpression(visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0]),
 					visitExprOrOpArgNodeExpression(opApplNode.getArgs()[1]));
diff --git a/src/test/java/de/tla2b/expression/SimpleExpressionTest.java b/src/test/java/de/tla2b/expression/SimpleExpressionTest.java
index 7f4553833e0fe7f8661d8a032a507fd4097ac30f..ac8f716bdcd1bae95876e8d82359bec92afb967c 100644
--- a/src/test/java/de/tla2b/expression/SimpleExpressionTest.java
+++ b/src/test/java/de/tla2b/expression/SimpleExpressionTest.java
@@ -32,6 +32,11 @@ public class SimpleExpressionTest {
 		compareExpr("1.0 : REAL", "1.0 \\in Real");
 	}
 
+	@Test
+	public void testRealDivisionExpression() throws Exception {
+		compareExpr("1.0 / 2.0", "1.0 / 2.0");
+	}
+
 	@Test
 	public void testExist() throws Exception {
 		compareExpr("#a.(a : {1} & 2 > 1)", "\\E a \\in {1}: 2 > 1");
diff --git a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleReals.java b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleReals.java
index f154d7ee5c0450e77bfa36ceb63370afe60337fd..7926e6a218199162455fe8b1b5695e32b0a10051 100644
--- a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleReals.java
+++ b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleReals.java
@@ -133,6 +133,17 @@ public class TestModuleReals {
 		TestUtil.typeCheckString(module);
 	}
 
+	@Test
+	public void testRealDivision() throws TLA2BException {
+		final String module = "-------------- MODULE Testing ----------------\n"
+			+ "EXTENDS Reals \n"
+			+ "CONSTANTS k \n"
+			+ "ASSUME k = 1.0 / 1.0 \n"
+			+ "=================================";
+		TestTypeChecker t = TestUtil.typeCheckString(module);
+		assertEquals("REAL", t.getConstantType("k"));
+	}
+
 	/*
 	 * Interval operator: x .. y
 	 */