>= became > = because of new >=
authornipkow
Wed, 01 Dec 2004 18:10:49 +0100
changeset 15353 b53b89d3bf03
parent 15352 cba05842bd7a
child 15354 9234f5765d9c
>= became > = because of new >=
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);