A few more revisions and explanations.

src/SI/ISQ_Quantities.thy

@@ -154,7 +154,10 @@ setup_lifting type_definition_QuantT
 text \<open> A dimension typed quantity is parameterised by two types: \<^typ>\<open>'a\<close>, the numeric type for the
   magntitude, and \<^typ>\<open>'d\<close> for the dimension expression, which is an element of \<^class>\<open>dim_type\<close>. 
   The type \<^typ>\<open>('n, 'd) QuantT\<close> is to \<^typ>\<open>'n Quantity\<close> as dimension types are to \<^typ>\<open>Dimension\<close>. 
-  Specifically, an element of \<^typ>\<open>('n', 'd) QuantT\<close> is a quantity whose dimension is \<^typ>\<open>'d\<close>. \<close>
+  Specifically, an element of \<^typ>\<open>('n', 'd) QuantT\<close> is a quantity whose dimension is \<^typ>\<open>'d\<close>.
+
+  Intuitively, the formula \<^term>\<open>x :: 'n['d]\<close> can be read as ``$x$ is a quantity of \<^typ>\<open>'d\<close>'',
+  for example it might be a quantity of length, or a quantity of mass. \<close>
 
 text \<open> Since quantities can have dimension type expressions that are distinct, but denote the same
   dimension, it is necessary to define the following function for coercion between two dimension

src/SI/SI_Accepted.thy

@@ -19,9 +19,14 @@ abbreviation degrees ("_\<degree>" [999] 999) where "n\<degree> \<equiv> n \<odo
 
 definition [si_def, si_eq]: "litre = 1/1000 \<odot> meter\<^sup>\<three>"
 
-abbreviation "tonne \<equiv> 10^3 \<odot> kilogram"
+definition [si_def, si_eq]: "tonne = 10^3 \<odot> kilogram"
 
-subsection \<open> Examples \<close>
+definition [si_def, si_eq]: "dalton = 1.66053906660 * (1 / 10^27) \<odot> kilogram"
+
+subsection \<open> Example Unit Equations \<close>
+
+lemma "1 \<odot> hour = 3600 \<odot> second"
+  by (si_simp)
 
 lemma "watt \<^bold>\<cdot> hour \<cong>\<^sub>Q 3600 \<odot> joule"   by (si_calc)
 

src/SI/SI_Constants.thy

@@ -47,15 +47,21 @@ text \<open> Elementary charge \<close>
 abbreviation elementary_charge :: "'a[I \<cdot> T]" ("\<^bold>e") where
   "elementary_charge \<equiv> (1.602176634 \<cdot> 1/(10^19)) \<odot> coulomb"
 
+text \<open> The Boltzmann constant \<close>
+
 abbreviation Boltzmann :: "'a[M \<cdot> L\<^sup>2 \<cdot> T\<^sup>-\<^sup>2 \<cdot> \<Theta>\<^sup>-\<^sup>1]" ("\<^bold>k") where
   "Boltzmann \<equiv> (1.380649\<cdot>1/(10^23)) \<odot> (joule \<^bold>/ kelvin)"
 
+text \<open> The Avogadro number \<close>
+
 abbreviation Avogadro :: "'a[N\<^sup>-\<^sup>1]" ("N\<^sub>A") where
 "Avogadro \<equiv> 6.02214076\<cdot>(10^23) \<odot> (mole\<^sup>-\<^sup>\<one>)"
 
 abbreviation max_luminous_frequency :: "'a[T\<^sup>-\<^sup>1]" where
 "max_luminous_frequency \<equiv> (540\<cdot>10^12) \<odot> hertz"
 
+text \<open> The luminous efficacy of monochromatic radiation of frequency \<^const>\<open>max_luminous_frequency\<close>. \<close>
+
 abbreviation luminous_efficacy :: "'a[J \<cdot> (L\<^sup>2 \<cdot> L\<^sup>-\<^sup>2) \<cdot> (M \<cdot> L\<^sup>2 \<cdot> T\<^sup>-\<^sup>3)\<^sup>-\<^sup>1]" ("K\<^sub>c\<^sub>d") where
 "luminous_efficacy \<equiv> 683 \<odot> (lumen\<^bold>/watt)"
 

src/SI/SI_Units.thy

@@ -4,6 +4,19 @@ theory SI_Units
   imports ISQ_Proof
 begin
 
+text \<open> An SI unit is simply a particular kind of quantity. \<close>
+
+type_synonym ('n, 'd) UnitT = "('n, 'd) QuantT"
+
+text \<open> Parallel to the seven base quantities, there are seven base units. In the implementation of
+  the SI unit system, we fix these to be precisely those quantities that have a base dimension
+  and a magnitude of \<^term>\<open>1\<close>. Consequently, a base unit corresponds to a unit in the algebraic
+  sense. \<close>
+
+lift_definition is_BaseUnit :: "'a::one['d::dim_type] \<Rightarrow> bool" 
+  is "\<lambda> x. mag x = 1 \<and> is_BaseDim (dim x)" .
+
+
 lift_definition mk_base_unit :: "'u itself \<Rightarrow> ('a::one)['u::dim_type]" 
   is "\<lambda> u. \<lparr> mag = 1, dim = QD('u) \<rparr>" by simp
 
@@ -13,7 +26,8 @@ translations "BUNIT('a)" == "CONST mk_base_unit TYPE('a)"
 lemma magQuant_mk [si_eq]: "\<lbrakk>BUNIT('u::dim_type)\<rbrakk>\<^sub>Q = 1"
   by (simp add: magQuant_def, transfer, simp)
 
-subsection \<open>Polymorphic Operations for SI Base Units \<close>
+text \<open> We now define the seven base units. Effectively, these definitions axiomatise give names
+  to the \<^term>\<open>1\<close> elements of the base quantities. \<close>
 
 definition [si_eq]: "meter    = BUNIT(L)"
 definition [si_eq]: "second   = BUNIT(T)"
@@ -30,9 +44,6 @@ type @{typ "real\<^sup>3"}. Note than when considering vectors, dimensions refer
 not to its components.
 \<close>
 
-lift_definition is_BaseUnit :: "'a::one['d::dim_type] \<Rightarrow> bool" 
-  is "\<lambda> x. mag x = 1 \<and> is_BaseDim (dim x)" .
-
 lemma meter_is_BaseUnit: "is_BaseUnit meter"
   by (simp add: si_eq, transfer, simp)