src/HOL/Lambda/ParRed.thy
changeset 1900 c7a869229091
parent 1789 aade046ec6d5
child 2159 e650a3f6f600
     1.1 --- a/src/HOL/Lambda/ParRed.thy	Fri Aug 02 12:25:26 1996 +0200
     1.2 +++ b/src/HOL/Lambda/ParRed.thy	Thu Aug 08 11:34:29 1996 +0200
     1.3 @@ -27,15 +27,15 @@
     1.4    deFun :: db => db
     1.5  
     1.6  primrec cd db
     1.7 -  cd_Var "cd(Var n) = Var n"
     1.8 -  cd_App "cd(s @ t) = (case s of
     1.9 +  "cd(Var n) = Var n"
    1.10 +  "cd(s @ t) = (case s of
    1.11              Var n => s @ (cd t) |
    1.12              s1 @ s2 => (cd s) @ (cd t) |
    1.13              Fun u => deFun(cd s)[cd t/0])"
    1.14 -  cd_Fun "cd(Fun s) = Fun(cd s)"
    1.15 +  "cd(Fun s) = Fun(cd s)"
    1.16  
    1.17  primrec deFun db
    1.18 -  deFun_Var "deFun(Var n) = Var n"
    1.19 -  deFun_App "deFun(s @ t) = s @ t"
    1.20 -  deFun_Fun "deFun(Fun s) = s"
    1.21 +  "deFun(Var n) = Var n"
    1.22 +  "deFun(s @ t) = s @ t"
    1.23 +  "deFun(Fun s) = s"
    1.24  end