Removed 8bit characters used by mistake
authoroheimb
Thu, 04 Apr 1996 13:28:50 +0200
changeset 1644 681f70ca3cf7
parent 1643 3f83b629f2e3
child 1645 be85d119a805
Removed 8bit characters used by mistake
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