--- 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 *)
--- 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
--- 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
--- 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,
--- 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
--- 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
--- 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
--- 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>
--- 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*)
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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