src/HOL/Lambda/Lambda.thy
changeset 19380 b808efaa5828
parent 19363 667b5ea637dd
child 19656 09be06943252
     1.1 --- a/src/HOL/Lambda/Lambda.thy	Sun Apr 09 18:51:11 2006 +0200
     1.2 +++ b/src/HOL/Lambda/Lambda.thy	Sun Apr 09 18:51:13 2006 +0200
     1.3 @@ -63,9 +63,9 @@
     1.4    "s ->> t == (s, t) \<in> beta^*"
     1.5  
     1.6  abbreviation (latex)
     1.7 -  beta_red :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>" 50)
     1.8 +  beta_red1 :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>" 50)
     1.9    "op \<rightarrow>\<^sub>\<beta> == op ->"
    1.10 -  beta_reds :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>\<^sup>*" 50)
    1.11 +  beta_reds1 :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>\<^sup>*" 50)
    1.12    "op \<rightarrow>\<^sub>\<beta>\<^sup>* == op ->>"
    1.13  
    1.14  inductive beta