--- a/src/HOLCF/Fix.ML Mon Dec 18 13:09:17 1995 +0100
+++ b/src/HOLCF/Fix.ML Wed Dec 20 16:28:51 1995 +0100
@@ -547,8 +547,8 @@
(* flat types are chain_finite *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "flat_imp_chain_finite" Fix.thy [flat_def,chain_finite_def]
- "flat(x::'a)==>chain_finite(x::'a)"
+qed_goalw "flat_imp_chain_finite" Fix.thy [is_flat_def,chain_finite_def]
+ "is_flat(x::'a)==>chain_finite(x::'a)"
(fn prems =>
[
(rewrite_goals_tac [max_in_chain_def]),
@@ -585,9 +585,9 @@
val adm_flat = flat_imp_chain_finite RS adm_chain_finite;
-(* flat(?x::?'a) ==> adm(?P::?'a => bool) *)
+(* is_flat(?x::?'a) ==> adm(?P::?'a => bool) *)
-qed_goalw "flat_void" Fix.thy [flat_def] "flat(UU::void)"
+qed_goalw "flat_void" Fix.thy [is_flat_def] "is_flat(UU::void)"
(fn prems =>
[
(strip_tac 1),
@@ -672,9 +672,9 @@
(atac 1)
]);
-qed_goalw "flat2flat" Fix.thy [flat_def]
-"!!f g.[|flat(x::'a); !y.f`(g`y)=(y::'b) ; !x.g`(f`x)=(x::'a) |] \
-\ ==> flat(y::'b)"
+qed_goalw "flat2flat" Fix.thy [is_flat_def]
+"!!f g.[|is_flat(x::'a); !y.f`(g`y)=(y::'b) ; !x.g`(f`x)=(x::'a) |] \
+\ ==> is_flat(y::'b)"
(fn prems =>
[
(strip_tac 1),
@@ -703,8 +703,8 @@
(* a result about functions with flat codomain *)
(* ------------------------------------------------------------------------- *)
-qed_goalw "flat_codom" Fix.thy [flat_def]
-"[|flat(y::'b);f`(x::'a)=(c::'b)|] ==> f`(UU::'a)=(UU::'b) | (!z.f`(z::'a)=c)"
+qed_goalw "flat_codom" Fix.thy [is_flat_def]
+"[|is_flat(y::'b);f`(x::'a)=(c::'b)|] ==> f`(UU::'a)=(UU::'b) | (!z.f`(z::'a)=c)"
(fn prems =>
[
(cut_facts_tac prems 1),
--- a/src/HOLCF/Fix.thy Mon Dec 18 13:09:17 1995 +0100
+++ b/src/HOLCF/Fix.thy Wed Dec 20 16:28:51 1995 +0100
@@ -18,7 +18,7 @@
adm :: "('a=>bool)=>bool"
admw :: "('a=>bool)=>bool"
chain_finite :: "'a=>bool"
-flat :: "'a=>bool"
+is_flat :: "'a=>bool"
defs
@@ -35,7 +35,7 @@
chain_finite_def "chain_finite (x::'a)==
!Y. is_chain (Y::nat=>'a) --> (? n.max_in_chain n Y)"
-flat_def "flat (x::'a) ==
+is_flat_def "is_flat (x::'a) ==
! x y. (x::'a) << y --> (x = UU) | (x=y)"
end
--- a/src/HOLCF/One.ML Mon Dec 18 13:09:17 1995 +0100
+++ b/src/HOLCF/One.ML Wed Dec 20 16:28:51 1995 +0100
@@ -68,7 +68,7 @@
(* one is flat *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "flat_one" One.thy [flat_def] "flat(one)"
+qed_goalw "flat_one" One.thy [is_flat_def] "is_flat(one)"
(fn prems =>
[
(rtac allI 1),
--- a/src/HOLCF/README Mon Dec 18 13:09:17 1995 +0100
+++ b/src/HOLCF/README Wed Dec 20 16:28:51 1995 +0100
@@ -19,6 +19,6 @@
28.06.95 The old uncurried version of HOLCF is no longer supported
in the distribution.
-18.08.95 added sections axioms, ops, domain, genertated
- and 8bit support
+18.08.95 added sections axioms, ops, domain, generated
+ and optional 8bit support
--- a/src/HOLCF/README.html Mon Dec 18 13:09:17 1995 +0100
+++ b/src/HOLCF/README.html Wed Dec 20 16:28:51 1995 +0100
@@ -1,6 +1,6 @@
<HTML><HEAD><TITLE>HOLCF/ReadMe</TITLE></HEAD><BODY>
-<H2>HOLCF: A higher order version of LCF based on Isabelle HOL</H2>
+<H3>HOLCF: A higher order version of LCF based on Isabelle HOL</H3>
Author: Franz Regensburger<BR>
Copyright 1995 Technische Universität München<P>
@@ -8,12 +8,19 @@
Version: 2.0<BR>
Date: 16.08.95<P>
-A detailed description of the entire development can be found in
+A detailed description (in german) of the entire development can be found in
<UL>
-<LI>Franz Regensburger,<BR>
- HOLCF: Eine konservative Erweiterung von HOL um LCF,<BR>
- Dissertation, Technische Universität München, 1994
+ <li> <A HREF="http://www4.informatik.tu-muenchen.de/papers/Diss_Regensbu.ps.gz"> HOLCF: eine konservative Erweiterung von HOL um LCF</A>, <br>
+ <A HREF="http://www4.informatik.tu-muenchen.de/~regensbu/">
+ Franz Regenburger</A>. <br>
+ Dissertation Technische Universität München. <BR>
+ Year: 1994.
+</UL>
+
+A short survey is available in
+<UL>
+<li><A HREF="http://www4.informatik.tu-muenchen.de/papers/Regensburger_HOLT1995.ps.gz">HOLCF: Higher Order Logic of Computable Functions</A> <br>
</UL>
Changes:
@@ -30,7 +37,10 @@
in the distribution.
<DT>18.08.95
-<DD>added sections axioms, ops, domain, genertated
- and 8bit support
+<DD>added sections axioms, ops, domain, generated
+ and optional 8bit support
</DL>
</BODY></HTML>
+
+
+
--- a/src/HOLCF/Tr1.ML Mon Dec 18 13:09:17 1995 +0100
+++ b/src/HOLCF/Tr1.ML Wed Dec 20 16:28:51 1995 +0100
@@ -123,7 +123,7 @@
(* type tr is flat *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "flat_tr" Tr1.thy [flat_def] "flat(TT)"
+qed_goalw "flat_tr" Tr1.thy [is_flat_def] "is_flat(TT)"
(fn prems =>
[
(rtac allI 1),
--- a/src/HOLCF/explicit_domains/Dnat.ML Mon Dec 18 13:09:17 1995 +0100
+++ b/src/HOLCF/explicit_domains/Dnat.ML Wed Dec 20 16:28:51 1995 +0100
@@ -499,7 +499,7 @@
]);
-qed_goalw "dnat_flat" Dnat.thy [flat_def] "flat(dzero)"
+qed_goalw "dnat_flat" Dnat.thy [is_flat_def] "is_flat(dzero)"
(fn prems =>
[
(rtac allI 1),