src/HOL/Lambda/Lambda.thy

--- a/src/HOL/Lambda/Lambda.thy	Thu Oct 25 22:59:11 2001 +0200
+++ b/src/HOL/Lambda/Lambda.thy	Fri Oct 26 12:24:19 2001 +0200
@@ -16,6 +16,9 @@
   | App dB dB (infixl "$" 200)
   | Abs dB
 
+syntax (symbols)
+  App :: "dB => dB => dB"    (infixl "\<^sub>\<degree>" 200)
+
 consts
   subst :: "[dB, dB, nat] => dB"  ("_[_'/_]" [300, 0, 0] 300)
   lift :: "[dB, nat] => dB"