--- a/src/HOL/Nat.thy Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Nat.thy Fri Sep 05 00:41:01 2014 +0200
@@ -89,12 +89,12 @@
| Suc pred
where
"pred (0 \<Colon> nat) = (0 \<Colon> nat)"
- apply atomize_elim
- apply (rename_tac n, induct_tac n rule: nat_induct0, auto)
- apply (simp add: Suc_def Nat_Abs_Nat_inject Nat_Rep_Nat Suc_RepI
- Suc_Rep_inject' Rep_Nat_inject)
-apply (simp only: Suc_not_Zero)
-done
+ apply atomize_elim
+ apply (rename_tac n, induct_tac n rule: nat_induct0, auto)
+ apply (simp add: Suc_def Nat_Abs_Nat_inject Nat_Rep_Nat Suc_RepI Suc_Rep_inject'
+ Rep_Nat_inject)
+ apply (simp only: Suc_not_Zero)
+ done
-- {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
setup {* Sign.mandatory_path "old" *}