
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 \<Rightarrow> 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 \<Rightarrow> nat) \<Rightarrow> 'f gterm set"
 inductive "well_formed_gterm arity"




