src/HOL/Nat.thy
changeset 58189 9d714be4f028
parent 57983 6edc3529bb4e
child 58306 117ba6cbe414
     1.1 --- a/src/HOL/Nat.thy	Fri Sep 05 00:41:01 2014 +0200
     1.2 +++ b/src/HOL/Nat.thy	Fri Sep 05 00:41:01 2014 +0200
     1.3 @@ -89,12 +89,12 @@
     1.4    | Suc pred
     1.5  where
     1.6    "pred (0 \<Colon> nat) = (0 \<Colon> nat)"
     1.7 -  apply atomize_elim
     1.8 -  apply (rename_tac n, induct_tac n rule: nat_induct0, auto)
     1.9 - apply (simp add: Suc_def Nat_Abs_Nat_inject Nat_Rep_Nat Suc_RepI
    1.10 -   Suc_Rep_inject' Rep_Nat_inject)
    1.11 -apply (simp only: Suc_not_Zero)
    1.12 -done
    1.13 +    apply atomize_elim
    1.14 +    apply (rename_tac n, induct_tac n rule: nat_induct0, auto)
    1.15 +   apply (simp add: Suc_def Nat_Abs_Nat_inject Nat_Rep_Nat Suc_RepI Suc_Rep_inject'
    1.16 +     Rep_Nat_inject)
    1.17 +  apply (simp only: Suc_not_Zero)
    1.18 +  done
    1.19  
    1.20  -- {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
    1.21  setup {* Sign.mandatory_path "old" *}