--- a/src/HOL/Lambda/ParRed.thy Wed Jul 15 11:15:57 1998 +0200
+++ b/src/HOL/Lambda/ParRed.thy Wed Jul 15 12:02:19 1998 +0200
@@ -19,26 +19,16 @@
intrs
var "Var n => Var n"
abs "s => t ==> Abs s => Abs t"
- app "[| s => s'; t => t' |] ==> s @ t => s' @ t'"
- beta "[| s => s'; t => t' |] ==> (Abs s) @ t => s'[t'/0]"
+ app "[| s => s'; t => t' |] ==> s $ t => s' $ t'"
+ beta "[| s => s'; t => t' |] ==> (Abs s) $ t => s'[t'/0]"
consts
cd :: dB => dB
recdef cd "measure size"
"cd(Var n) = Var n"
- "cd(Var n @ t) = Var n @ cd t"
- "cd((s1 @ s2) @ t) = cd(s1 @ s2) @ cd t"
- "cd(Abs u @ t) = (cd u)[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(Var n $ t) = Var n $ cd t"
+ "cd((s1 $ s2) $ t) = cd(s1 $ s2) $ cd t"
+ "cd(Abs u $ t) = (cd u)[cd t/0]"
"cd(Abs s) = Abs(cd s)"
-(*
-primrec deAbs dB
- "deAbs(Var n) = Var n"
- "deAbs(s @ t) = s @ t"
- "deAbs(Abs s) = s"*)
end