src/HOL/Lambda/ParRed.thy
changeset 19363 667b5ea637dd
parent 19086 1b3780be6cc2
child 20503 503ac4c5ef91
     1.1 --- a/src/HOL/Lambda/ParRed.thy	Sat Apr 08 22:12:02 2006 +0200
     1.2 +++ b/src/HOL/Lambda/ParRed.thy	Sat Apr 08 22:51:06 2006 +0200
     1.3 @@ -17,9 +17,9 @@
     1.4  consts
     1.5    par_beta :: "(dB \<times> dB) set"
     1.6  
     1.7 -abbreviation (output)
     1.8 +abbreviation
     1.9    par_beta_red :: "[dB, dB] => bool"  (infixl "=>" 50)
    1.10 -  "(s => t) = ((s, t) \<in> par_beta)"
    1.11 +  "s => t == (s, t) \<in> par_beta"
    1.12  
    1.13  inductive par_beta
    1.14    intros