forked from Isabelle_DOF/Isabelle_DOF
hint to a dimension bug...
This commit is contained in:
parent
890eee8b24
commit
f7f1a0d10d
|
@ -445,6 +445,8 @@ definition degree :: "real[meter / meter]" where
|
||||||
abbreviation degrees ("_\<degree>" [999] 999) where "n\<degree> \<equiv> n\<cdot>degree"
|
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> meter\<^sup>\<two>"
|
||||||
|
definition [si_def]: "litre' = 1/1000 \<cdot> (Unit_cube meter)"
|
||||||
|
|
||||||
|
|
||||||
definition [si_def]: "pint = 0.56826125 \<cdot> litre"
|
definition [si_def]: "pint = 0.56826125 \<cdot> litre"
|
||||||
|
|
||||||
|
|
Reference in New Issue