src/HOL/Lambda/ParRed.thy
changeset 5146 1ea751ae62b2
parent 5134 51f81581e3d9
child 8624 69619f870939
     1.1 --- a/src/HOL/Lambda/ParRed.thy	Wed Jul 15 11:15:57 1998 +0200
     1.2 +++ b/src/HOL/Lambda/ParRed.thy	Wed Jul 15 12:02:19 1998 +0200
     1.3 @@ -19,26 +19,16 @@
     1.4    intrs
     1.5      var   "Var n => Var n"
     1.6      abs   "s => t ==> Abs s => Abs t"
     1.7 -    app   "[| s => s'; t => t' |] ==> s @ t => s' @ t'"
     1.8 -    beta  "[| s => s'; t => t' |] ==> (Abs s) @ t => s'[t'/0]"
     1.9 +    app   "[| s => s'; t => t' |] ==> s $ t => s' $ t'"
    1.10 +    beta  "[| s => s'; t => t' |] ==> (Abs s) $ t => s'[t'/0]"
    1.11  
    1.12  consts
    1.13    cd  :: dB => dB
    1.14  
    1.15  recdef cd "measure size"
    1.16    "cd(Var n) = Var n"
    1.17 -  "cd(Var n @ t) = Var n @ cd t"
    1.18 -  "cd((s1 @ s2) @ t) = cd(s1 @ s2) @ cd t"
    1.19 -  "cd(Abs u @ t) = (cd u)[cd t/0]"
    1.20 -(*
    1.21 -  "cd(s @ t) = (case s of Var n   => (s @ cd t)
    1.22 -                        | s1 @ s2 => (cd s @ cd t) 
    1.23 -                        | Abs u   => deAbs(cd s)[cd t/0])"
    1.24 -*)
    1.25 +  "cd(Var n     $ t) = Var n $ cd t"
    1.26 +  "cd((s1 $ s2) $ t) = cd(s1 $ s2) $ cd t"
    1.27 +  "cd(Abs u     $ t) = (cd u)[cd t/0]"
    1.28    "cd(Abs s) = Abs(cd s)"
    1.29 -(*
    1.30 -primrec deAbs dB
    1.31 -  "deAbs(Var n) = Var n"
    1.32 -  "deAbs(s @ t) = s @ t"
    1.33 -  "deAbs(Abs s) = s"*)
    1.34  end