src/HOL/Fun.thy
changeset 12460 624a8cd51b4e
parent 12459 6978ab7cac64
child 13585 db4005b40cc6
     1.1 --- a/src/HOL/Fun.thy	Mon Dec 10 20:59:43 2001 +0100
     1.2 +++ b/src/HOL/Fun.thy	Tue Dec 11 13:43:00 2001 +0100
     1.3 @@ -77,7 +77,7 @@
     1.4    funcset :: "['a set, 'b set] => ('a => 'b) set"      (infixr 60)
     1.5    "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a => 'b)"  ("(3%_:_./ _)" [0, 0, 3] 3)
     1.6  syntax (xsymbols)
     1.7 -  "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a => 'b)"  ("(3\\<lambda>_\<in>_./ _)" [0, 0, 3] 3)
     1.8 +  "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a => 'b)"  ("(3\\<lambda>_\\<in>_./ _)" [0, 0, 3] 3)
     1.9  
    1.10    (*Giving funcset an arrow syntax (-> or =>) clashes with many existing theories*)
    1.11