# HG changeset patch
# User oheimb
# Date 828617330 -7200
# Node ID 681f70ca3cf72961218ebb2e1734b7a348d68813
# Parent  3f83b629f2e37a2bbf2f1c21ab152aee88f3dab3
Removed 8bit characters used by mistake

diff -r 3f83b629f2e3 -r 681f70ca3cf7 src/HOLCF/domain/theorems.ML
--- 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