src/HOL/Fun.thy
changeset 12114 a8e860c86252
parent 11609 3f3d1add4d94
child 12258 5da24e7e9aba
     1.1 --- a/src/HOL/Fun.thy	Fri Nov 09 00:06:15 2001 +0100
     1.2 +++ b/src/HOL/Fun.thy	Fri Nov 09 00:09:47 2001 +0100
     1.3 @@ -46,7 +46,7 @@
     1.4    inj_on :: ['a => 'b, 'a set] => bool
     1.5      "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y"
     1.6  
     1.7 -syntax (symbols)
     1.8 +syntax (xsymbols)
     1.9    "op o"        :: "['b => 'c, 'a => 'b, 'a] => 'c"      (infixl "\\<circ>" 55)
    1.10  
    1.11  syntax
    1.12 @@ -79,7 +79,7 @@
    1.13  
    1.14    (*Giving funcset the arrow syntax (namely ->) clashes with other theories*)
    1.15  
    1.16 -syntax (symbols)
    1.17 +syntax (xsymbols)
    1.18    "@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\\<Pi> _\\<in>_./ _)"   10)
    1.19  
    1.20  translations