minimal changes due to revisions
This commit is contained in:
parent
818b9c9b4c
commit
75b6baea53
|
@ -23,6 +23,7 @@ abbreviation "tonne \<equiv> 10^3 \<odot> kilogram"
|
|||
|
||||
subsection \<open> Examples \<close>
|
||||
|
||||
declare[[show_types]]
|
||||
lemma "watt \<^bold>\<cdot> hour \<cong>\<^sub>Q 3600 \<odot> joule"
|
||||
by (si_calc)
|
||||
|
||||
|
|
|
@ -31,7 +31,7 @@ definition [si_eq]: "gram = milli \<odot> kilogram"
|
|||
|
||||
text\<open>The full beauty of the approach is perhaps revealed here, with the
|
||||
type of a classical three-dimensional gravitation field:\<close>
|
||||
type_synonym gravitation_field = "(real\<^sup>3 \<Rightarrow> real\<^sup>3)[L \<cdot> T\<^sup>-\<^sup>2]"
|
||||
type_synonym gravitation_field = "real\<^sup>3[L] \<Rightarrow> (real\<^sup>3[L \<cdot> T\<^sup>-\<^sup>2])"
|
||||
|
||||
subsection \<open> Properties \<close>
|
||||
|
||||
|
|
|
@ -1,7 +1,7 @@
|
|||
section \<open> SI Quantities \<close>
|
||||
|
||||
theory SI_Quantities
|
||||
imports SI_Units Optics.Lenses
|
||||
imports SI_Units (* Optics.Lenses *)
|
||||
begin
|
||||
|
||||
|
||||
|
|
|
@ -217,11 +217,13 @@ subsubsection \<open> SI base type constructors \<close>
|
|||
|
||||
text\<open>We embed the basic SI types into the SI type expressions: \<close>
|
||||
|
||||
|
||||
instantiation Length :: si_baseunit
|
||||
begin
|
||||
definition si_sem_Length :: "Length itself \<Rightarrow> Unit"
|
||||
where [si_def]: "si_sem_Length x = 1\<lparr>Meters := 1\<rparr>"
|
||||
instance by (intro_classes, auto simp add: si_sem_Length_def is_BaseUnit_def, (transfer, simp)+)
|
||||
instance
|
||||
by (intro_classes, auto simp add: si_sem_Length_def is_BaseUnit_def, (transfer, simp)+)
|
||||
end
|
||||
|
||||
instantiation Mass :: si_baseunit
|
||||
|
|
Loading…
Reference in New Issue