author | paulson |
Mon, 21 Apr 1997 10:38:46 +0200 | |
changeset 3001 | 8f89a99d2b00 |
parent 3000 | 7ecb8b6a3d7f |
child 3002 | 223e5d65faaa |
--- a/src/HOL/Lambda/ParRed.thy Mon Apr 21 10:16:41 1997 +0200 +++ b/src/HOL/Lambda/ParRed.thy Mon Apr 21 10:38:46 1997 +0200 @@ -28,10 +28,9 @@ primrec cd dB "cd(Var n) = Var n" - "cd(s @ t) = (case s of - Var n => s @ (cd t) | - s1 @ s2 => (cd s) @ (cd t) | - Abs u => deAbs(cd s)[cd t/0])" + "cd(s @ t) = (case s of Var n => (s @ cd t) + | s1 @ s2 => (cd s @ cd t) + | Abs u => deAbs(cd s)[cd t/0])" "cd(Abs s) = Abs(cd s)" primrec deAbs dB