src/HOL/Nat.thy
changeset 58306 117ba6cbe414
parent 58189 9d714be4f028
child 58377 c6f93b8d2d8e
     1.1 --- a/src/HOL/Nat.thy	Thu Sep 11 18:54:36 2014 +0200
     1.2 +++ b/src/HOL/Nat.thy	Thu Sep 11 18:54:36 2014 +0200
     1.3 @@ -96,10 +96,10 @@
     1.4    apply (simp only: Suc_not_Zero)
     1.5    done
     1.6  
     1.7 --- {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
     1.8 +-- {* Avoid name clashes by prefixing the output of @{text old_rep_datatype} with @{text old}. *}
     1.9  setup {* Sign.mandatory_path "old" *}
    1.10  
    1.11 -rep_datatype "0 \<Colon> nat" Suc
    1.12 +old_rep_datatype "0 \<Colon> nat" Suc
    1.13    apply (erule nat_induct0, assumption)
    1.14   apply (rule nat.inject)
    1.15  apply (rule nat.distinct(1))