src/HOL/Library/FuncSet.thy
changeset 19656 09be06943252
parent 19536 1a3a3cf8b4fa
child 19736 d8d0f8f51d69
     1.1 --- a/src/HOL/Library/FuncSet.thy	Tue May 16 21:32:56 2006 +0200
     1.2 +++ b/src/HOL/Library/FuncSet.thy	Tue May 16 21:33:01 2006 +0200
     1.3 @@ -23,9 +23,8 @@
     1.4    funcset :: "['a set, 'b set] => ('a => 'b) set"      (infixr "->" 60)
     1.5    "A -> B == Pi A (%_. B)"
     1.6  
     1.7 -abbreviation (xsymbols)
     1.8 -  funcset1  (infixr "\<rightarrow>" 60)
     1.9 -  "funcset1 == funcset"
    1.10 +const_syntax (xsymbols)
    1.11 +  funcset  (infixr "\<rightarrow>" 60)
    1.12  
    1.13  syntax
    1.14    "@Pi"  :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3PI _:_./ _)" 10)