src/HOL/Nonstandard_Analysis/StarDef.thy

--- a/src/HOL/Nonstandard_Analysis/StarDef.thy	Mon Jan 29 11:54:44 2024 +0100
+++ b/src/HOL/Nonstandard_Analysis/StarDef.thy	Mon Jan 29 19:35:07 2024 +0000
@@ -768,6 +768,9 @@
 instance star :: (idom) idom ..
 instance star :: (idom_divide) idom_divide ..
 
+instance star :: (divide_trivial) divide_trivial
+  by (intro_classes; transfer) simp_all
+
 instance star :: (division_ring) division_ring
   by (intro_classes; transfer) (simp_all add: divide_inverse)