--- a/src/HOLCF/Cprod3.thy Mon Dec 02 12:19:56 1996 +0100
+++ b/src/HOLCF/Cprod3.thy Mon Dec 02 12:37:15 1996 +0100
@@ -82,9 +82,6 @@
(* reverse translation <= does not work yet !! *)
(* start 8bit 1 *)
-translations
- "Let x = a in e" == "CLet`a`(¤ x.e)"
-
(* end 8bit 1 *)
end
--- a/src/HOLCF/Pcpo.thy Mon Dec 02 12:19:56 1996 +0100
+++ b/src/HOLCF/Pcpo.thy Mon Dec 02 12:37:15 1996 +0100
@@ -14,11 +14,5 @@
inst_void_pcpo "(UU::void) = UU_void"
(* start 8bit 1 *)
-syntax
- "GUU" :: "'a::pcpo" ("Ø")
-
-translations
- "Ø" == "UU"
-
(* end 8bit 1 *)
end
--- a/src/HOLCF/Porder.thy Mon Dec 02 12:19:56 1996 +0100
+++ b/src/HOLCF/Porder.thy Mon Dec 02 12:37:15 1996 +0100
@@ -43,13 +43,6 @@
lub "lub(S) = (@x. S <<| x)"
(* start 8bit 1 *)
-
-syntax
- "Glub" :: "[pttrn, 'a] => 'a" ("(3×_./ _)" 10)
-
-translations
- "×x.t" == "lub(range(%x.t))"
-
(* end 8bit 1 *)
end
--- a/src/HOLCF/Porder0.thy Mon Dec 02 12:19:56 1996 +0100
+++ b/src/HOLCF/Porder0.thy Mon Dec 02 12:37:15 1996 +0100
@@ -40,12 +40,6 @@
inst_void_po "((op <<)::[void,void]=>bool) = less_void"
(* start 8bit 1 *)
-syntax
- "Ý" :: "['a,'a::po] => bool" (infixl 55)
-
-translations
- "x Ý y" == "x << y"
-
(* end 8bit 1 *)
end
--- a/src/HOLCF/Sprod0.thy Mon Dec 02 12:19:56 1996 +0100
+++ b/src/HOLCF/Sprod0.thy Mon Dec 02 12:37:15 1996 +0100
@@ -51,14 +51,6 @@
&(! a b. ~a=UU & ~b=UU & p=Ispair a b --> z=b)"
(* start 8bit 1 *)
-types
-
-('a, 'b) "õ" (infixr 20)
-
-translations
-
-(type) "x õ y" == (type) "x ** y"
-
(* end 8bit 1 *)
end
--- a/src/HOLCF/Sprod3.thy Mon Dec 02 12:19:56 1996 +0100
+++ b/src/HOLCF/Sprod3.thy Mon Dec 02 12:37:15 1996 +0100
@@ -34,12 +34,6 @@
ssplit_def "ssplit == (LAM f. strictify`(LAM p.f`(sfst`p)`(ssnd`p)))"
(* start 8bit 1 *)
-syntax
- "@Gstuple" :: "['a, args] => 'a ** 'b" ("(1É_,/ _Ê)")
-
-translations
- "Éx, y, zÊ" == "Éx, Éy, zÊÊ"
- "Éx, yÊ" == "(|x,y|)"
(* end 8bit 1 *)
end
--- a/src/HOLCF/Ssum0.thy Mon Dec 02 12:19:56 1996 +0100
+++ b/src/HOLCF/Ssum0.thy Mon Dec 02 12:37:15 1996 +0100
@@ -52,14 +52,6 @@
&(!b. b~=UU & s=Isinr(b) --> z=g`b)"
(* start 8bit 1 *)
-types
-
-('a, 'b) "ó" (infixr 10)
-
-translations
-
-(type) "x ó y" == (type) "x ++ y"
-
(* end 8bit 1 *)
end
--- a/src/HOLCF/Ssum3.thy Mon Dec 02 12:19:56 1996 +0100
+++ b/src/HOLCF/Ssum3.thy Mon Dec 02 12:37:15 1996 +0100
@@ -30,9 +30,6 @@
"case s of sinl`x => t1 | sinr`y => t2" == "sswhen`(LAM x.t1)`(LAM y.t2)`s"
(* start 8bit 1 *)
-translations
-"case s of sinl`x => t1 | sinr`y => t2" == "sswhen`(¤x.t1)`(¤y.t2)`s"
-
(* end 8bit 1 *)
end
--- a/src/HOLCF/Tr1.thy Mon Dec 02 12:19:56 1996 +0100
+++ b/src/HOLCF/Tr1.thy Mon Dec 02 12:37:15 1996 +0100
@@ -43,14 +43,6 @@
(LAM e1 e2 t. sswhen`(LAM x.e1)`(LAM y.e2)`(rep_tr`t))"
(* start 8bit 1 *)
-syntax
- "GeqTT" :: "tr => bool" ("(Å_Æ)")
- "GeqFF" :: "tr => bool" ("(Ç_È)")
-
-translations
- "ÅxÆ" == "x = TT"
- "ÇxÈ" == "x = FF"
-
(* end 8bit 1 *)
--- a/src/HOLCF/Up3.thy Mon Dec 02 12:19:56 1996 +0100
+++ b/src/HOLCF/Up3.thy Mon Dec 02 12:37:15 1996 +0100
@@ -29,9 +29,6 @@
"case l of up`x => t1" == "fup`(LAM x.t1)`l"
(* start 8bit 1 *)
-translations
-
-"case l of up`x => t1" == "fup`(¤x.t1)`l"
(* end 8bit 1 *)
end