src/HOL/Lambda/Lambda.thy
changeset 19363 667b5ea637dd
parent 19086 1b3780be6cc2
child 19380 b808efaa5828
     1.1 --- a/src/HOL/Lambda/Lambda.thy	Sat Apr 08 22:12:02 2006 +0200
     1.2 +++ b/src/HOL/Lambda/Lambda.thy	Sat Apr 08 22:51:06 2006 +0200
     1.3 @@ -56,15 +56,17 @@
     1.4  consts
     1.5    beta :: "(dB \<times> dB) set"
     1.6  
     1.7 -abbreviation (output)
     1.8 +abbreviation
     1.9    beta_red :: "[dB, dB] => bool"  (infixl "->" 50)
    1.10 -  "(s -> t) = ((s, t) \<in> beta)"
    1.11 +  "s -> t == (s, t) \<in> beta"
    1.12    beta_reds :: "[dB, dB] => bool"  (infixl "->>" 50)
    1.13 -  "(s ->> t) = ((s, t) \<in> beta^*)"
    1.14 +  "s ->> t == (s, t) \<in> beta^*"
    1.15  
    1.16 -syntax (latex)
    1.17 +abbreviation (latex)
    1.18    beta_red :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>" 50)
    1.19 +  "op \<rightarrow>\<^sub>\<beta> == op ->"
    1.20    beta_reds :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>\<^sup>*" 50)
    1.21 +  "op \<rightarrow>\<^sub>\<beta>\<^sup>* == op ->>"
    1.22  
    1.23  inductive beta
    1.24    intros