--- a/src/HOLCF/domain/theorems.ML Thu Apr 04 12:58:47 1996 +0200
+++ b/src/HOLCF/domain/theorems.ML Thu Apr 04 13:28:50 1996 +0200
@@ -56,10 +56,11 @@
(* ----- general proofs ----------------------------------------------------- *)
val quant_ss = HOL_ss addsimps (map (fn s => prove_goal HOL.thy s (fn _ =>[
- fast_tac HOL_cs 1]))["(Âx. P x À Q)=((Âx. P x) À Q)",
- "(Âx. P À Q x) = (P À (Âx. Q x))"]);
+ fast_tac HOL_cs 1]))["(!x. P x & Q)=((!x. P x) & Q)",
+ "(!x. P & Q x) = (P & (!x. Q x))"]);
-val all2E = prove_goal HOL.thy "Ë Âx y . P x y; P x y êë R Ì êë R" (fn prems =>[
+val all2E = prove_goal HOL.thy "[| !x y . P x y; P x y ==> R |] ==> R"
+ (fn prems =>[
resolve_tac prems 1,
cut_facts_tac prems 1,
fast_tac HOL_cs 1]);
@@ -70,13 +71,13 @@
dtac notnotD 1,
etac (hd prems) 1]);
-val dist_eqI = prove_goal Porder.thy "¿ x Ý y êë x Û y" (fn prems => [
+val dist_eqI = prove_goal Porder.thy "~ x << y ==> x ~= y" (fn prems => [
rtac swap3 1,
etac (antisym_less_inverse RS conjunct1) 1,
resolve_tac prems 1]);
-val cfst_strict = prove_goal Cprod3.thy "cfst`Ø = Ø" (fn _ => [
+val cfst_strict = prove_goal Cprod3.thy "cfst`UU = UU" (fn _ => [
(simp_tac (HOLCF_ss addsimps [inst_cprod_pcpo2]) 1)]);
-val csnd_strict = prove_goal Cprod3.thy "csnd`Ø = Ø" (fn _ => [
+val csnd_strict = prove_goal Cprod3.thy "csnd`UU = UU" (fn _ => [
(simp_tac (HOLCF_ss addsimps [inst_cprod_pcpo2]) 1)]);
in