src/HOL/Lambda/ParRed.thy
changeset 3001 8f89a99d2b00
parent 2159 e650a3f6f600
child 5134 51f81581e3d9
     1.1 --- a/src/HOL/Lambda/ParRed.thy	Mon Apr 21 10:16:41 1997 +0200
     1.2 +++ b/src/HOL/Lambda/ParRed.thy	Mon Apr 21 10:38:46 1997 +0200
     1.3 @@ -28,10 +28,9 @@
     1.4  
     1.5  primrec cd dB
     1.6    "cd(Var n) = Var n"
     1.7 -  "cd(s @ t) = (case s of
     1.8 -            Var n => s @ (cd t) |
     1.9 -            s1 @ s2 => (cd s) @ (cd t) |
    1.10 -            Abs u => deAbs(cd s)[cd t/0])"
    1.11 +  "cd(s @ t) = (case s of Var n   => (s @ cd t)
    1.12 +                        | s1 @ s2 => (cd s @ cd t) 
    1.13 +                        | Abs u   => deAbs(cd s)[cd t/0])"
    1.14    "cd(Abs s) = Abs(cd s)"
    1.15  
    1.16  primrec deAbs dB