src/HOL/Lambda/Eta.thy
changeset 19363 667b5ea637dd
parent 19086 1b3780be6cc2
child 19380 b808efaa5828
     1.1 --- a/src/HOL/Lambda/Eta.thy	Sat Apr 08 22:12:02 2006 +0200
     1.2 +++ b/src/HOL/Lambda/Eta.thy	Sat Apr 08 22:51:06 2006 +0200
     1.3 @@ -21,13 +21,13 @@
     1.4  consts
     1.5    eta :: "(dB \<times> dB) set"
     1.6  
     1.7 -abbreviation (output)
     1.8 +abbreviation
     1.9    eta_red :: "[dB, dB] => bool"   (infixl "-e>" 50)
    1.10 -  "(s -e> t) = ((s, t) \<in> eta)"
    1.11 +  "s -e> t == (s, t) \<in> eta"
    1.12    eta_reds :: "[dB, dB] => bool"   (infixl "-e>>" 50)
    1.13 -  "(s -e>> t) = ((s, t) \<in> eta^*)"
    1.14 +  "s -e>> t == (s, t) \<in> eta^*"
    1.15    eta_red0 :: "[dB, dB] => bool"   (infixl "-e>=" 50)
    1.16 -  "(s -e>= t) = ((s, t) \<in> eta^=)"
    1.17 +  "s -e>= t == (s, t) \<in> eta^="
    1.18  
    1.19  inductive eta
    1.20    intros
    1.21 @@ -224,12 +224,13 @@
    1.22  consts
    1.23    par_eta :: "(dB \<times> dB) set"
    1.24  
    1.25 -abbreviation (output)
    1.26 +abbreviation
    1.27    par_eta_red :: "[dB, dB] => bool"   (infixl "=e>" 50)
    1.28 -  "(s =e> t) = ((s, t) \<in> par_eta)"
    1.29 +  "s =e> t == (s, t) \<in> par_eta"
    1.30  
    1.31 -syntax (xsymbols)
    1.32 +abbreviation (xsymbols)
    1.33    par_eta_red :: "[dB, dB] => bool"   (infixl "\<Rightarrow>\<^sub>\<eta>" 50)
    1.34 +  "op \<Rightarrow>\<^sub>\<eta> == op =e>"
    1.35  
    1.36  inductive par_eta
    1.37  intros