# HG changeset patch # User paulson # Date 861611926 -7200 # Node ID 8f89a99d2b009cc1ded6b18e54829cb023810277 # Parent 7ecb8b6a3d7fefbca975f899c1de58923bf349af Tidied up the indentation diff -r 7ecb8b6a3d7f -r 8f89a99d2b00 src/HOL/Lambda/ParRed.thy --- 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