src/HOL/Nat.thy
changeset 55469 b19dd108f0c2
parent 55468 98b25c51e9e5
child 55534 b18bdcbda41b
     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,9 @@
     1.4  apply (iprover elim: Nat_Abs_Nat_inverse [THEN subst])
     1.5  done
     1.6  
     1.7 -free_constructors ["0 \<Colon> nat", Suc] case_nat [=] [[], [pred]] [[pred: "0 \<Colon> nat"]]
     1.8 +free_constructors case_nat for
     1.9 +    =: "0 \<Colon> nat" (defaults pred: "0 \<Colon> nat")
    1.10 +  | Suc pred
    1.11    apply atomize_elim
    1.12    apply (rename_tac n, induct_tac n rule: nat_induct0, auto)
    1.13   apply (simp add: Suc_def Nat_Abs_Nat_inject Nat_Rep_Nat Suc_RepI