# HG changeset patch
# User regensbu
# Date 819473331 -3600
# Node ID 324aa813463903614341644e0bbc8213dd5f8e2c
# Parent 3cc3fde8d005751c644709749e98a20ec5b4f50b
changed predicate flat to is_flat in theory Fix.thy
diff -r 3cc3fde8d005 -r 324aa8134639 src/HOLCF/Fix.ML
--- 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),
diff -r 3cc3fde8d005 -r 324aa8134639 src/HOLCF/Fix.thy
--- 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
diff -r 3cc3fde8d005 -r 324aa8134639 src/HOLCF/One.ML
--- 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),
diff -r 3cc3fde8d005 -r 324aa8134639 src/HOLCF/README
--- 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
diff -r 3cc3fde8d005 -r 324aa8134639 src/HOLCF/README.html
--- 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 @@
HOLCF/ReadMe
-HOLCF: A higher order version of LCF based on Isabelle HOL
+HOLCF: A higher order version of LCF based on Isabelle HOL
Author: Franz Regensburger
Copyright 1995 Technische Universität München
@@ -8,12 +8,19 @@
Version: 2.0
Date: 16.08.95
-A detailed description of the entire development can be found in
+A detailed description (in german) of the entire development can be found in
+
+A short survey is available in
+
Changes:
@@ -30,7 +37,10 @@
in the distribution.
18.08.95
-added sections axioms, ops, domain, genertated
- and 8bit support
+added sections axioms, ops, domain, generated
+ and optional 8bit support
+
+
+
diff -r 3cc3fde8d005 -r 324aa8134639 src/HOLCF/Tr1.ML
--- 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),
diff -r 3cc3fde8d005 -r 324aa8134639 src/HOLCF/explicit_domains/Dnat.ML
--- 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),