src/HOL/Num.thy
changeset 61169 4de9ff3ea29a
parent 60758 d8d85a8172b5
child 61630 608520e0e8e2
     1.1 --- a/src/HOL/Num.thy	Sun Sep 13 22:25:21 2015 +0200
     1.2 +++ b/src/HOL/Num.thy	Sun Sep 13 22:56:52 2015 +0200
     1.3 @@ -106,7 +106,7 @@
     1.4    "m < n \<longleftrightarrow> nat_of_num m < nat_of_num n"
     1.5  
     1.6  instance
     1.7 -  by (default, auto simp add: less_num_def less_eq_num_def num_eq_iff)
     1.8 +  by standard (auto simp add: less_num_def less_eq_num_def num_eq_iff)
     1.9  
    1.10  end
    1.11