nicolas.meric
/
Isabelle_DOF
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

little game with scalar type

This commit is contained in:
Burkhart Wolff 2022-08-04 11:31:53 +02:00
parent 5a06d3618b
commit 66f78001eb
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
examples/CENELEC_50128/mini_odo/mini_odo.thy
View File

@ -225,8 +225,8 @@ consts Accel::"distance_function \<Rightarrow> real[s] \<Rightarrow> real[
consts Speed\<^sub>M\<^sub>a\<^sub>x::"real[m\<cdot>s\<^sup>-\<^sup>1]"
(* Non - SI conform common abrbreviations *)
definition "kmh \<equiv> kilo *\<^sub>Q metre \<^bold>/ hour :: real[m\<cdot>s\<^sup>-\<^sup>1]"
definition "kHz \<equiv> kilo *\<^sub>Q hertz :: real[s\<^sup>-\<^sup>1]"
definition "kmh \<equiv> kilo *\<^sub>Q metre \<^bold>/ hour :: 'a::{field,ring_char_0}[m\<cdot>s\<^sup>-\<^sup>1]"
definition "kHz \<equiv> kilo *\<^sub>Q hertz :: 'a::{field,ring_char_0}[s\<^sup>-\<^sup>1]"
(*>*)
text\<open>