changeset 18963 | 3adfc9dfb30a |
parent 18702 | 7dc7dcd63224 |
child 19602 | e25d1e9a0675 |
--- a/src/HOL/Wellfounded_Recursion.thy Mon Feb 06 21:02:01 2006 +0100 +++ b/src/HOL/Wellfounded_Recursion.thy Tue Feb 07 08:47:43 2006 +0100 @@ -290,10 +290,10 @@ code_primconst wfrec ml {* -fun wfrec f x = f (wfrec f) x; +fun `_` f x = f (`_` f) x; *} haskell {* -wfrec f x = f (wfrec f) x +`_` f x = f (`_` f) x *} (* code_syntax_const