# HG changeset patch
# User wenzelm
# Date 1201460670 -3600
# Node ID 3267d0694d932dc2e1c3b7639bcc8db4d73694db
# Parent  89a03048f312b7e41b12fb3f0cca5b0ffcda326c
tuned;

diff -r 89a03048f312 -r 3267d0694d93 src/FOL/ex/Nat.thy
--- a/src/FOL/ex/Nat.thy	Sun Jan 27 18:32:32 2008 +0100
+++ b/src/FOL/ex/Nat.thy	Sun Jan 27 20:04:30 2008 +0100
@@ -16,7 +16,7 @@
 consts
   0 :: nat    ("0")
   Suc :: "nat => nat"
-  rec :: "[nat, 'a, [nat,'a]=>'a] => 'a"
+  rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a"
   add :: "[nat, nat] => nat"    (infixl "+" 60)
 
 axioms
diff -r 89a03048f312 -r 3267d0694d93 src/FOL/ex/Natural_Numbers.thy
--- a/src/FOL/ex/Natural_Numbers.thy	Sun Jan 27 18:32:32 2008 +0100
+++ b/src/FOL/ex/Natural_Numbers.thy	Sun Jan 27 20:04:30 2008 +0100
@@ -33,13 +33,13 @@
   show "Suc(0) \<noteq> 0"
   proof
     assume "Suc(0) = 0"
-    thus False by (rule Suc_neq_0)
+    then show False by (rule Suc_neq_0)
   qed
   fix n assume hyp: "Suc(n) \<noteq> n"
   show "Suc(Suc(n)) \<noteq> Suc(n)"
   proof
     assume "Suc(Suc(n)) = Suc(n)"
-    hence "Suc(n) = n" by (rule Suc_inject)
+    then have "Suc(n) = n" by (rule Suc_inject)
     with hyp show False by contradiction
   qed
 qed
@@ -67,7 +67,7 @@
 lemma "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i + j) = i + f(j)"
 proof -
   assume "!!n. f(Suc(n)) = Suc(f(n))"
-  thus ?thesis by (induct i) simp_all
+  then show ?thesis by (induct i) simp_all
 qed
 
 end