--- a/src/HOL/Library/Numeral_Type.thy Fri Jan 12 17:58:03 2018 +0100
+++ b/src/HOL/Library/Numeral_Type.thy Sat Jan 13 09:18:54 2018 +0000
@@ -415,7 +415,7 @@
show univ_eq: "(UNIV :: 'a bit0 set) = set enum_class.enum"
unfolding enum_bit0_def type_definition.Abs_image[OF type_definition_bit0, symmetric]
- by (simp add: image_comp [symmetric] inj_on_Abs_bit0 card_image image_int_atLeast_lessThan)
+ by (simp add: image_comp [symmetric] inj_on_Abs_bit0 card_image image_int_atLeastLessThan)
(auto intro!: image_cong[OF refl] simp add: Abs_bit0'_def)
fix P :: "'a bit0 \<Rightarrow> bool"
@@ -439,7 +439,7 @@
show univ_eq: "(UNIV :: 'a bit1 set) = set enum_class.enum"
unfolding enum_bit1_def type_definition.Abs_image[OF type_definition_bit1, symmetric]
- by(simp add: image_comp [symmetric] inj_on_Abs_bit1 card_image image_int_atLeast_lessThan)
+ by(simp add: image_comp [symmetric] inj_on_Abs_bit1 card_image image_int_atLeastLessThan)
(auto intro!: image_cong[OF refl] simp add: Abs_bit1'_def)
fix P :: "'a bit1 \<Rightarrow> bool"