changeset 11679 | afdbee613f58 |
parent 11673 | 79e5536af6c4 |
child 11696 | 233362cfecc7 |
--- a/src/FOL/ex/Natural_Numbers.thy Thu Oct 04 15:28:26 2001 +0200 +++ b/src/FOL/ex/Natural_Numbers.thy Thu Oct 04 15:29:22 2001 +0200 @@ -18,7 +18,7 @@ axioms induct [induct type: nat]: - "P(0) \<Longrightarrow> (!!x. P(x) ==> P(Suc(x))) ==> P(n)" + "P(0) ==> (!!x. P(x) ==> P(Suc(x))) ==> P(n)" Suc_inject: "Suc(m) = Suc(n) ==> m = n" Suc_neq_0: "Suc(m) = 0 ==> R" rec_0: "rec(0, a, f) = a"