diff -r f5401162c9f0 -r ecdfd237ffee doc-src/TutorialI/Inductive/Advanced.thy --- a/doc-src/TutorialI/Inductive/Advanced.thy Mon Oct 08 14:19:42 2001 +0200 +++ b/doc-src/TutorialI/Inductive/Advanced.thy Mon Oct 08 14:29:02 2001 +0200 @@ -78,9 +78,9 @@ consts integer_arity :: "integer_op \ nat" primrec -"integer_arity (Number n) = #0" -"integer_arity UnaryMinus = #1" -"integer_arity Plus = #2" +"integer_arity (Number n) = 0" +"integer_arity UnaryMinus = 1" +"integer_arity Plus = 2" consts well_formed_gterm :: "('f \ nat) \ 'f gterm set" inductive "well_formed_gterm arity"