# HG changeset patch
# User nipkow
# Date 1101921049 -3600
# Node ID b53b89d3bf033c7d58c73158e50df94a25f281c9
# Parent  cba05842bd7af320c48bf5b010d673047d00519d
>= became > = because of new >=

diff -r cba05842bd7a -r b53b89d3bf03 src/HOLCF/Cprod3.ML
--- a/src/HOLCF/Cprod3.ML	Wed Dec 01 12:53:49 2004 +0100
+++ b/src/HOLCF/Cprod3.ML	Wed Dec 01 18:10:49 2004 +0100
@@ -133,7 +133,7 @@
 qed "beta_cfun_cprod";
 
 Goalw [cpair_def]
-        " <a,b>=<aa,ba>  ==> a=aa & b=ba";
+        " <a,b> = <aa,ba>  ==> a=aa & b=ba";
 by (dtac (beta_cfun_cprod RS subst) 1);
 by (dtac (beta_cfun_cprod RS subst) 1);
 by (etac Pair_inject 1);
@@ -169,7 +169,7 @@
 qed "cprodE";
 
 Goalw [cfst_def,cpair_def] 
-        "cfst$<x,y>=x";
+        "cfst$<x,y> = x";
 by (stac beta_cfun_cprod 1);
 by (stac beta_cfun 1);
 by (rtac cont_fst 1);
@@ -177,7 +177,7 @@
 qed "cfst2";
 
 Goalw [csnd_def,cpair_def] 
-        "csnd$<x,y>=y";
+        "csnd$<x,y> = y";
 by (stac beta_cfun_cprod 1);
 by (stac beta_cfun 1);
 by (rtac cont_snd 1);