--- 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
--- 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