# HG changeset patch
# User oheimb
# Date 849526635 -3600
# Node ID fbd14a05fb888352ec1afadef2e14f69b099805d
# Parent  e5c08f8b483b3c1962b4ca1c35da1ef118fe5bef
removed 8bit sections

diff -r e5c08f8b483b -r fbd14a05fb88 src/HOLCF/Cprod3.thy
--- 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
 
diff -r e5c08f8b483b -r fbd14a05fb88 src/HOLCF/Pcpo.thy
--- 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 
diff -r e5c08f8b483b -r fbd14a05fb88 src/HOLCF/Porder.thy
--- 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 
diff -r e5c08f8b483b -r fbd14a05fb88 src/HOLCF/Porder0.thy
--- 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 
diff -r e5c08f8b483b -r fbd14a05fb88 src/HOLCF/Sprod0.thy
--- 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
diff -r e5c08f8b483b -r fbd14a05fb88 src/HOLCF/Sprod3.thy
--- 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
diff -r e5c08f8b483b -r fbd14a05fb88 src/HOLCF/Ssum0.thy
--- 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
 
diff -r e5c08f8b483b -r fbd14a05fb88 src/HOLCF/Ssum3.thy
--- 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
diff -r e5c08f8b483b -r fbd14a05fb88 src/HOLCF/Tr1.thy
--- 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 *)
 
 
diff -r e5c08f8b483b -r fbd14a05fb88 src/HOLCF/Up3.thy
--- 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