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