From f7f1a0d10de3b94bee0b9c6b56894c224a5d383a Mon Sep 17 00:00:00 2001
From: bu <wolff@lri.fr>
Date: Tue, 10 Dec 2019 10:46:06 +0100
Subject: [PATCH] hint to a dimension bug...

---
 src/SI/Units.thy | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/SI/Units.thy b/src/SI/Units.thy
index 341e4d1..cc07d12 100644
--- a/src/SI/Units.thy
+++ b/src/SI/Units.thy
@@ -445,6 +445,8 @@ definition degree :: "real[meter / meter]" where
 abbreviation degrees ("_\<degree>" [999] 999) where "n\<degree> \<equiv> n\<cdot>degree" 
 
 definition [si_def]: "litre = 1/1000 \<cdot> meter\<^sup>\<two>"
+definition [si_def]: "litre' = 1/1000 \<cdot> (Unit_cube meter)"
+
 
 definition [si_def]: "pint = 0.56826125 \<cdot> litre"