1.1 --- a/src/HOL/Library/FuncSet.thy	Wed Apr 14 13:28:46 2004 +0200
     1.2 +++ b/src/HOL/Library/FuncSet.thy	Wed Apr 14 14:13:05 2004 +0200
     1.3 @@ -30,6 +30,10 @@
     1.4    funcset :: "['a set, 'b set] => ('a => 'b) set"  (infixr "\<rightarrow>" 60) 
     1.5    "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)"  ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
     1.6  
     1.7 +syntax (HTML output)
     1.8 +  "@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi> _\<in>_./ _)"   10)
     1.9 +  "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)"  ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
    1.10 +
    1.11  translations
    1.12    "PI x:A. B" => "Pi A (%x. B)"
    1.13    "A -> B"    => "Pi A (_K B)"