From 66f78001ebc041c38f9fa6166ef2bd0d505a9ab5 Mon Sep 17 00:00:00 2001
From: Burkhart Wolff <wolffburkhart@gmail.com>
Date: Thu, 4 Aug 2022 11:31:53 +0200
Subject: [PATCH] little game with scalar type

---
 examples/CENELEC_50128/mini_odo/mini_odo.thy | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/examples/CENELEC_50128/mini_odo/mini_odo.thy b/examples/CENELEC_50128/mini_odo/mini_odo.thy
index 532cca61..f2edc62b 100644
--- a/examples/CENELEC_50128/mini_odo/mini_odo.thy
+++ b/examples/CENELEC_50128/mini_odo/mini_odo.thy
@@ -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>