--- a/src/HOLCF/Tr.thy Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOLCF/Tr.thy Tue Jan 09 15:32:27 2001 +0100
@@ -27,14 +27,14 @@
"@orelse" :: "tr => tr => tr" ("_ orelse _" [31,30] 30)
translations
- "x andalso y" == "trand`x`y"
- "x orelse y" == "tror`x`y"
- "If b then e1 else e2 fi" == "Icifte`b`e1`e2"
+ "x andalso y" == "trand$x$y"
+ "x orelse y" == "tror$x$y"
+ "If b then e1 else e2 fi" == "Icifte$b$e1$e2"
defs
TT_def "TT==Def True"
FF_def "FF==Def False"
neg_def "neg == flift2 Not"
- ifte_def "Icifte == (LAM b t e. flift1(%b. if b then t else e)`b)"
+ ifte_def "Icifte == (LAM b t e. flift1(%b. if b then t else e)$b)"
andalso_def "trand == (LAM x y. If x then y else FF fi)"
orelse_def "tror == (LAM x y. If x then TT else y fi)"
If2_def "If2 Q x y == If Q then x else y fi"