# HG changeset patch
# User oheimb
# Date 850499158 -3600
# Node ID 91d8abf108be2a570f6197099f43fa91882b7384
# Parent  651fce76c86c4ad4da2a495c466c973484bd9a94
adaptions for symbol font

diff -r 651fce76c86c -r 91d8abf108be src/HOLCF/Cfun1.thy
--- a/src/HOLCF/Cfun1.thy	Fri Dec 13 18:40:50 1996 +0100
+++ b/src/HOLCF/Cfun1.thy	Fri Dec 13 18:45:58 1996 +0100
@@ -31,7 +31,14 @@
 
 translations "f`x" == "fapp f x"
 
+syntax (symbols)
+
+  "->"		:: [type, type] => type		("(_ \\<rightarrow>/ _)" [6,5]5)
+  "LAM "	:: "[idts, 'a => 'b] => ('a -> 'b)"
+					("(3\\<Lambda>_./ _)" [0, 10] 10)
+
 defs 
+
   Cfun_def      "Cfun == {f. cont(f)}"
 
 rules
@@ -47,11 +54,4 @@
   (*defining the abstract constants*)
   less_cfun_def         "less_cfun fo1 fo2 == ( fapp fo1 << fapp fo2 )"
 
-(* start 8bit 1 *)
-(* end 8bit 1 *)
-
-
 end
-
-(* start 8bit 2 *)
-(* end 8bit 2 *)
diff -r 651fce76c86c -r 91d8abf108be src/HOLCF/Cprod3.thy
--- a/src/HOLCF/Cprod3.thy	Fri Dec 13 18:40:50 1996 +0100
+++ b/src/HOLCF/Cprod3.thy	Fri Dec 13 18:45:58 1996 +0100
@@ -44,7 +44,7 @@
 
    and
 
-   ¤<x,y,z>.e
+   LAM <x,y,z>.e
 *)
 
 types
@@ -81,8 +81,6 @@
   "LAM <x,y>.b"      == "csplit`(LAM x.LAM y.b)"
   (* reverse translation <= does not work yet !! *)
 
-(* start 8bit 1 *)
-(* end 8bit 1 *)
 end
 
 
diff -r 651fce76c86c -r 91d8abf108be src/HOLCF/Lift1.thy
--- a/src/HOLCF/Lift1.thy	Fri Dec 13 18:40:50 1996 +0100
+++ b/src/HOLCF/Lift1.thy	Fri Dec 13 18:45:58 1996 +0100
@@ -10,7 +10,7 @@
 
 default term
 
-datatype 'a lift  = Undef | Def('a)
+datatype 'a lift = Undef | Def 'a
 
 arities "lift" :: (term)term
 
diff -r 651fce76c86c -r 91d8abf108be src/HOLCF/Pcpo.ML
--- a/src/HOLCF/Pcpo.ML	Fri Dec 13 18:40:50 1996 +0100
+++ b/src/HOLCF/Pcpo.ML	Fri Dec 13 18:45:58 1996 +0100
@@ -34,7 +34,7 @@
 (* [| is_chain(?S5); range(?S5) <| ?x1 |] ==> lub(range(?S5)) << ?x1        *)
 
 qed_goal "maxinch_is_thelub" Pcpo.thy "is_chain Y ==> \
-\	max_in_chain i Y = (lub(range(Y)) = ((Y i)::'a::pcpo))" 
+\       max_in_chain i Y = (lub(range(Y)) = ((Y i)::'a::pcpo))" 
 (fn prems => 
 	[
 	cut_facts_tac prems 1,
diff -r 651fce76c86c -r 91d8abf108be src/HOLCF/Pcpo.thy
--- a/src/HOLCF/Pcpo.thy	Fri Dec 13 18:40:50 1996 +0100
+++ b/src/HOLCF/Pcpo.thy	Fri Dec 13 18:45:58 1996 +0100
@@ -1,18 +1,22 @@
 Pcpo = Porder +
 
 classes pcpo < po
+
 arities void :: pcpo
 
-consts  
-        UU :: "'a::pcpo"        
+consts
+
+  UU		:: "'a::pcpo"        
+
+syntax (symbols)
+
+  UU		:: "'a::pcpo"				("\\<bottom>")
 
 rules
 
-        minimal "UU << x"       
-        cpo     "is_chain(S) ==> ? x. range(S) <<| (x::'a::pcpo)" 
+  minimal	"UU << x"       
+  cpo		"is_chain S ==> ? x. range(S) <<| (x::'a::pcpo)" 
 
 inst_void_pcpo  "(UU::void) = UU_void"
 
-(* start 8bit 1 *)
-(* end 8bit 1 *)
 end 
diff -r 651fce76c86c -r 91d8abf108be src/HOLCF/Porder.thy
--- a/src/HOLCF/Porder.thy	Fri Dec 13 18:40:50 1996 +0100
+++ b/src/HOLCF/Porder.thy	Fri Dec 13 18:45:58 1996 +0100
@@ -18,6 +18,18 @@
         max_in_chain :: "[nat,nat=>'a::po]=>bool"
         finite_chain :: "(nat=>'a::po)=>bool"
 
+syntax
+
+  "@LUB"	:: "(('b::term) => 'a) => 'a"	(binder "LUB " 10)
+
+translations
+
+  "LUB x. t"	== "lub(range(%x.t))"
+
+syntax (symbols)
+
+  "LUB "	:: "[idts, 'a] => 'a"		("(3\\<Squnion>_./ _)"[0,10] 10)
+
 defs
 
 (* class definitions *)
@@ -27,23 +39,20 @@
 
 
 (* Arbitrary chains are total orders    *)                  
-is_tord         "is_tord(S) == ! x y. x:S & y:S --> (x<<y | y<<x)"
+is_tord         "is_tord S == ! x y. x:S & y:S --> (x<<y | y<<x)"
 
 (* Here we use countable chains and I prefer to code them as functions! *)
-is_chain        "is_chain(F) == (! i.F(i) << F(Suc(i)))"
+is_chain        "is_chain F == (! i.F(i) << F(Suc(i)))"
 
 (* finite chains, needed for monotony of continouous functions *)
 
 max_in_chain_def "max_in_chain i C == ! j. i <= j --> C(i) = C(j)" 
 
-finite_chain_def "finite_chain(C) == is_chain(C) & (? i. max_in_chain i C)"
+finite_chain_def "finite_chain C == is_chain(C) & (? i. max_in_chain i C)"
 
 rules
 
-lub             "lub(S) = (@x. S <<| x)"
-
-(* start 8bit 1 *)
-(* end 8bit 1 *)
+lub             "lub S = (@x. S <<| x)"
 
 end 
 
diff -r 651fce76c86c -r 91d8abf108be src/HOLCF/Porder0.thy
--- a/src/HOLCF/Porder0.thy	Fri Dec 13 18:40:50 1996 +0100
+++ b/src/HOLCF/Porder0.thy	Fri Dec 13 18:45:58 1996 +0100
@@ -20,13 +20,19 @@
 
 arities void :: po
 
-consts  "<<"    ::      "['a,'a::po] => bool"   (infixl 55)
+consts
+
+  "<<"		:: "['a,'a::po] => bool"	(infixl 55)
+
+syntax (symbols)
+
+  "op <<"	:: "['a,'a::po] => bool"	(infixl "\\<sqsubseteq>" 55)
 
 rules
 
 (* class axioms: justification is theory Void *)
 
-refl_less       "x << x"        
+refl_less       "x<<x"        
                                 (* witness refl_less_void    *)
 
 antisym_less    "[|x<<y ; y<<x |] ==> x = y"    
@@ -39,9 +45,6 @@
 
 inst_void_po    "((op <<)::[void,void]=>bool) = less_void"
 
-(* start 8bit 1 *)
-(* end 8bit 1 *)
-
 end 
 
 
diff -r 651fce76c86c -r 91d8abf108be src/HOLCF/README.html
--- a/src/HOLCF/README.html	Fri Dec 13 18:40:50 1996 +0100
+++ b/src/HOLCF/README.html	Fri Dec 13 18:45:58 1996 +0100
@@ -38,7 +38,7 @@
 
 <DT>18.08.95
 <DD>added sections axioms, ops, domain, generated
-    and optional 8bit support
+    and optional 8bit symbolic font support
 </DL>
 </BODY></HTML>
 
diff -r 651fce76c86c -r 91d8abf108be src/HOLCF/ROOT.ML
--- a/src/HOLCF/ROOT.ML	Fri Dec 13 18:40:50 1996 +0100
+++ b/src/HOLCF/ROOT.ML	Fri Dec 13 18:45:58 1996 +0100
@@ -8,14 +8,8 @@
 *)
 
 val banner = "HOLCF with sections axioms,ops,domain,generated";
-init_thy_reader();
+writeln banner;
 
-(* start 8bit 1 *)
-val banner = 
-        "HOLCF with sections axioms,ops,domain,generated and 8bit characters";
-(* end 8bit 1 *)
-
-writeln banner;
 print_depth 1;
 
 use_thy "HOLCF";
@@ -40,11 +34,10 @@
 init_thy_reader();
 init_pps ();
 
-print_depth 100;  
-make_html:=false;
-
 fun qed_spec_mp name =
   let val thm = normalize_thm [RSspec,RSmp] (result())
   in bind_thm(name, thm) end;
 
+print_depth 10;  
+
 val HOLCF_build_completed = (); (*indicate successful build*)
diff -r 651fce76c86c -r 91d8abf108be src/HOLCF/Sprod0.thy
--- a/src/HOLCF/Sprod0.thy	Fri Dec 13 18:40:50 1996 +0100
+++ b/src/HOLCF/Sprod0.thy	Fri Dec 13 18:45:58 1996 +0100
@@ -14,6 +14,10 @@
 
 arities "**" :: (pcpo,pcpo)term 
 
+syntax (symbols)
+ 
+  "**"		:: [type, type] => type		("(_ \\<otimes>/ _)" [21,20] 20)
+
 consts
   Sprod         :: "('a => 'b => bool)set"
   Spair_Rep     :: "['a,'b] => ['a,'b] => bool"
@@ -50,8 +54,6 @@
                                         (p=Ispair UU UU  --> z=UU)
                 &(! a b. ~a=UU & ~b=UU & p=Ispair a b    --> z=b)"  
 
-(* start 8bit 1 *)
-(* end 8bit 1 *)
 
 end
 
diff -r 651fce76c86c -r 91d8abf108be src/HOLCF/Sprod3.thy
--- a/src/HOLCF/Sprod3.thy	Fri Dec 13 18:40:50 1996 +0100
+++ b/src/HOLCF/Sprod3.thy	Fri Dec 13 18:45:58 1996 +0100
@@ -11,18 +11,21 @@
 arities "**" :: (pcpo,pcpo)pcpo                 (* Witness sprod2.ML *)
 
 consts  
-        spair        :: "'a -> 'b -> ('a**'b)" (* continuous strict pairing *)
-        sfst         :: "('a**'b)->'a"
-        ssnd         :: "('a**'b)->'b"
-        ssplit       :: "('a->'b->'c)->('a**'b)->'c"
+  spair		:: "'a -> 'b -> ('a**'b)" (* continuous strict pairing *)
+  sfst		:: "('a**'b)->'a"
+  ssnd		:: "('a**'b)->'b"
+  ssplit	:: "('a->'b->'c)->('a**'b)->'c"
 
 syntax  
-        "@stuple"    :: "['a, args] => 'a ** 'b"        ("(1'(|_,/ _|'))")
+  "@stuple"	:: "['a, args] => 'a ** 'b"		("(1'(|_,/ _|'))")
 
 translations
         "(|x, y, z|)"   == "(|x, (|y, z|)|)"
         "(|x, y|)"      == "spair`x`y"
 
+syntax (symbols)
+  "@stuple"	:: "['a, args] => 'a ** 'b"		("(1É_,/ _Ê)")
+
 rules 
 
 inst_sprod_pcpo "(UU::'a**'b) = Ispair UU UU"
@@ -33,8 +36,6 @@
 ssnd_def        "ssnd   == (LAM p.Issnd p)"     
 ssplit_def      "ssplit == (LAM f. strictify`(LAM p.f`(sfst`p)`(ssnd`p)))"
 
-(* start 8bit 1 *)
-(* end 8bit 1 *)
 
 end
 
diff -r 651fce76c86c -r 91d8abf108be src/HOLCF/Ssum0.thy
--- a/src/HOLCF/Ssum0.thy	Fri Dec 13 18:40:50 1996 +0100
+++ b/src/HOLCF/Ssum0.thy	Fri Dec 13 18:45:58 1996 +0100
@@ -14,6 +14,10 @@
 
 arities "++" :: (pcpo,pcpo)term 
 
+syntax (symbols)
+
+  "++"		:: [type, type] => type		("(_ \\<oplus>/ _)" [21, 20] 20)
+
 consts
   Ssum          :: "(['a,'b,bool]=>bool)set"
   Sinl_Rep      :: "['a,'a,'b,bool]=>bool"
@@ -51,7 +55,5 @@
                         &(!a. a~=UU & s=Isinl(a) --> z=f`a)  
                         &(!b. b~=UU & s=Isinr(b) --> z=g`b)"  
 
-(* start 8bit 1 *)
-(* end 8bit 1 *)
 end
 
diff -r 651fce76c86c -r 91d8abf108be src/HOLCF/Ssum3.thy
--- a/src/HOLCF/Ssum3.thy	Fri Dec 13 18:40:50 1996 +0100
+++ b/src/HOLCF/Ssum3.thy	Fri Dec 13 18:45:58 1996 +0100
@@ -29,7 +29,4 @@
 translations
 "case s of sinl`x => t1 | sinr`y => t2" == "sswhen`(LAM x.t1)`(LAM y.t2)`s"
 
-(* start 8bit 1 *)
-(* end 8bit 1 *)
-
 end
diff -r 651fce76c86c -r 91d8abf108be src/HOLCF/Tr1.thy
--- a/src/HOLCF/Tr1.thy	Fri Dec 13 18:40:50 1996 +0100
+++ b/src/HOLCF/Tr1.thy	Fri Dec 13 18:45:58 1996 +0100
@@ -42,8 +42,4 @@
   tr_when_def "tr_when == 
         (LAM e1 e2 t. sswhen`(LAM x.e1)`(LAM y.e2)`(rep_tr`t))"
 
-(* start 8bit 1 *)
-(* end 8bit 1 *)
-
-
 end
diff -r 651fce76c86c -r 91d8abf108be src/HOLCF/Up3.thy
--- a/src/HOLCF/Up3.thy	Fri Dec 13 18:40:50 1996 +0100
+++ b/src/HOLCF/Up3.thy	Fri Dec 13 18:45:58 1996 +0100
@@ -28,9 +28,6 @@
 
 "case l of up`x => t1" == "fup`(LAM x.t1)`l"
 
-(* start 8bit 1 *)
-(* end 8bit 1 *)
-
 end