src/HOL/Nat.thy
changeset 55468 98b25c51e9e5
parent 55443 3def821deb70
child 55469 b19dd108f0c2
     1.1 --- a/src/HOL/Nat.thy	Fri Feb 14 07:53:46 2014 +0100
     1.2 +++ b/src/HOL/Nat.thy	Fri Feb 14 07:53:46 2014 +0100
     1.3 @@ -82,7 +82,7 @@
     1.4  apply (iprover elim: Nat_Abs_Nat_inverse [THEN subst])
     1.5  done
     1.6  
     1.7 -wrap_free_constructors ["0 \<Colon> nat", Suc] case_nat [=] [[], [pred]] [[pred: "0 \<Colon> nat"]]
     1.8 +free_constructors ["0 \<Colon> nat", Suc] case_nat [=] [[], [pred]] [[pred: "0 \<Colon> nat"]]
     1.9    apply atomize_elim
    1.10    apply (rename_tac n, induct_tac n rule: nat_induct0, auto)
    1.11   apply (simp add: Suc_def Nat_Abs_Nat_inject Nat_Rep_Nat Suc_RepI
    1.12 @@ -101,7 +101,7 @@
    1.13  
    1.14  setup {* Sign.parent_path *}
    1.15  
    1.16 --- {* But erase the prefix for properties that are not generated by @{text wrap_free_constructors}. *}
    1.17 +-- {* But erase the prefix for properties that are not generated by @{text free_constructors}. *}
    1.18  setup {* Sign.mandatory_path "nat" *}
    1.19  
    1.20  declare