src/HOL/Fun.thy
changeset 14565 c6dc17aab88a
parent 13910 f9a9ef16466f
child 15111 c108189645f8
     1.1 --- a/src/HOL/Fun.thy	Wed Apr 14 13:28:46 2004 +0200
     1.2 +++ b/src/HOL/Fun.thy	Wed Apr 14 14:13:05 2004 +0200
     1.3 @@ -52,6 +52,8 @@
     1.4  
     1.5  syntax (xsymbols)
     1.6    comp :: "['b => 'c, 'a => 'b, 'a] => 'c"        (infixl "\<circ>" 55)
     1.7 +syntax (HTML output)
     1.8 +  comp :: "['b => 'c, 'a => 'b, 'a] => 'c"        (infixl "\<circ>" 55)
     1.9  
    1.10  
    1.11  constdefs