| changeset 21210 | c17fd2df4e9e |
| parent 20770 | 2c583720436e |
| child 21404 | eb85850d3eb7 |
--- a/src/HOL/Library/FuncSet.thy Tue Nov 07 11:47:56 2006 +0100 +++ b/src/HOL/Library/FuncSet.thy Tue Nov 07 11:47:57 2006 +0100 @@ -23,7 +23,7 @@ funcset :: "['a set, 'b set] => ('a => 'b) set" (infixr "->" 60) "A -> B == Pi A (%_. B)" -const_syntax (xsymbols) +notation (xsymbols) funcset (infixr "\<rightarrow>" 60) syntax