src/HOL/Lambda/Eta.thy
changeset 19380 b808efaa5828
parent 19363 667b5ea637dd
child 19656 09be06943252
     1.1 --- a/src/HOL/Lambda/Eta.thy	Sun Apr 09 18:51:11 2006 +0200
     1.2 +++ b/src/HOL/Lambda/Eta.thy	Sun Apr 09 18:51:13 2006 +0200
     1.3 @@ -229,7 +229,7 @@
     1.4    "s =e> t == (s, t) \<in> par_eta"
     1.5  
     1.6  abbreviation (xsymbols)
     1.7 -  par_eta_red :: "[dB, dB] => bool"   (infixl "\<Rightarrow>\<^sub>\<eta>" 50)
     1.8 +  par_eta_red1 :: "[dB, dB] => bool"   (infixl "\<Rightarrow>\<^sub>\<eta>" 50)
     1.9    "op \<Rightarrow>\<^sub>\<eta> == op =e>"
    1.10  
    1.11  inductive par_eta