# HG changeset patch # User wenzelm # Date 1002202162 -7200 # Node ID afdbee613f582a16dea805beb964a5adaa5769a8 # Parent 6aa3e2d266830fcbb23475f862147ed9118f3f17 unsymbolized; diff -r 6aa3e2d26683 -r afdbee613f58 src/FOL/ex/Natural_Numbers.thy --- 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) \ (!!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"