author wenzelm Wed, 15 Nov 2006 20:50:23 +0100 changeset 21392 e571e84cbe89 parent 21391 a8809f46bd7f child 21393 c648e24fd7ee
tuned proofs;
```--- a/src/HOL/ex/Abstract_NAT.thy	Wed Nov 15 20:50:22 2006 +0100
+++ b/src/HOL/ex/Abstract_NAT.thy	Wed Nov 15 20:50:23 2006 +0100
@@ -43,7 +43,7 @@
case zero
show "\<exists>!y. ?R zero y"
proof
-      show "?R zero e" by (rule Rec_zero)
+      show "?R zero e" ..
fix y assume "?R zero y"
then show "y = e" by cases simp_all
qed
@@ -54,7 +54,7 @@
and yy': "\<And>y'. ?R m y' \<Longrightarrow> y = y'" by blast
show "\<exists>!z. ?R (succ m) z"
proof
-      from y show "?R (succ m) (r m y)" by (rule Rec_succ)
+      from y show "?R (succ m) (r m y)" ..
fix z assume "?R (succ m) z"
then obtain u where "z = r m u" and "?R m u" by cases simp_all
with yy' show "z = r m y" by (simp only:)
@@ -77,7 +77,7 @@

lemma rec_zero [simp]: "rec e r zero = e"
proof (rule rec_eval)
-  show "Rec e r zero e" by (rule Rec_zero)
+  show "Rec e r zero e" ..
qed

lemma rec_succ [simp]: "rec e r (succ m) = r m (rec e r m)"
@@ -85,7 +85,7 @@
let ?R = "Rec e r"
have "?R m (rec e r m)"
unfolding rec_def using Rec_functional by (rule theI')
-  then show "?R (succ m) (r m (rec e r m))" by (rule Rec_succ)
+  then show "?R (succ m) (r m (rec e r m))" ..
qed

@@ -108,6 +108,10 @@