--- a/src/HOL/Nonstandard_Analysis/HyperDef.thy Sat Jun 22 06:25:34 2019 +0000
+++ b/src/HOL/Nonstandard_Analysis/HyperDef.thy Sat Jun 22 07:18:55 2019 +0000
@@ -253,11 +253,11 @@
by (simp add: star_of_def [symmetric])
declaration \<open>
- K (Lin_Arith.add_inj_thms [@{thm star_of_le} RS iffD2,
- @{thm star_of_less} RS iffD2, @{thm star_of_eq} RS iffD2]
- #> Lin_Arith.add_simps [@{thm star_of_zero}, @{thm star_of_one},
- @{thm star_of_numeral}, @{thm star_of_add},
- @{thm star_of_minus}, @{thm star_of_diff}, @{thm star_of_mult}]
+ K (Lin_Arith.add_simps @{thms star_of_zero star_of_one
+ star_of_numeral star_of_add
+ star_of_minus star_of_diff star_of_mult}
+ #> Lin_Arith.add_inj_thms @{thms star_of_le [THEN iffD2]
+ star_of_less [THEN iffD2] star_of_eq [THEN iffD2]}
#> Lin_Arith.add_inj_const (\<^const_name>\<open>StarDef.star_of\<close>, \<^typ>\<open>real \<Rightarrow> hypreal\<close>))
\<close>