removed 8bit sections
authoroheimb
Mon, 02 Dec 1996 12:37:15 +0100
changeset 2291 fbd14a05fb88
parent 2290 e5c08f8b483b
child 2292 c1c5652600f1
removed 8bit sections
src/HOLCF/Cprod3.thy
src/HOLCF/Pcpo.thy
src/HOLCF/Porder.thy
src/HOLCF/Porder0.thy
src/HOLCF/Sprod0.thy
src/HOLCF/Sprod3.thy
src/HOLCF/Ssum0.thy
src/HOLCF/Ssum3.thy
src/HOLCF/Tr1.thy
src/HOLCF/Up3.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
 
--- 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