src/HOL/Number_Theory/Euclidean_Algorithm.thy
changeset 60580 7e741e22d7fc
parent 60526 fad653acf58f
child 60582 d694f217ee41
     1.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Thu Jun 25 22:56:33 2015 +0200
     1.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Thu Jun 25 23:33:47 2015 +0200
     1.3 @@ -1527,14 +1527,19 @@
     1.4  definition [simp]:
     1.5    "normalization_factor_int = (sgn :: int \<Rightarrow> int)"
     1.6  
     1.7 -instance proof
     1.8 -  case goal2 then show ?case by (auto simp add: abs_mult nat_mult_distrib)
     1.9 +instance
    1.10 +proof (default, goals)
    1.11 +  case 2
    1.12 +  then show ?case by (auto simp add: abs_mult nat_mult_distrib)
    1.13  next
    1.14 -  case goal3 then show ?case by (simp add: zsgn_def)
    1.15 +  case 3
    1.16 +  then show ?case by (simp add: zsgn_def)
    1.17  next
    1.18 -  case goal5 then show ?case by (auto simp: zsgn_def)
    1.19 +  case 5
    1.20 +  then show ?case by (auto simp: zsgn_def)
    1.21  next
    1.22 -  case goal6 then show ?case by (auto split: abs_split simp: zsgn_def)
    1.23 +  case 6
    1.24 +  then show ?case by (auto split: abs_split simp: zsgn_def)
    1.25  qed (auto simp: sgn_times split: abs_split)
    1.26  
    1.27  end