src/HOL/Prod.ML

   [ (rtac minor 1),
     (rtac (major RS SigmaD1) 1),
     (rtac (major RS SigmaD2) 1) ]);
 
 val prems = goal Prod.thy
-    "[| A<=C;  !!x. x:A ==> B<=D |] ==> Sigma A (%x.B) <= Sigma C (%x.D)";
+    "[| A<=C;  !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D";
 by (cut_facts_tac prems 1);
 by (fast_tac (set_cs addIs (prems RL [subsetD]) 
                      addSIs [SigmaI] 
                      addSEs [SigmaE]) 1);
 qed "Sigma_mono";
 
 qed_goal "Sigma_empty1" Prod.thy "Sigma {} B = {}"
  (fn _ => [ (fast_tac (eq_cs addSEs [SigmaE]) 1) ]);
 
-qed_goal "Sigma_empty2" Prod.thy "Sigma A (%x.{}) = {}"
+qed_goal "Sigma_empty2" Prod.thy "A Times {} = {}"
  (fn _ => [ (fast_tac (eq_cs addSEs [SigmaE]) 1) ]);
 
 Addsimps [Sigma_empty1,Sigma_empty2]; 
 
 goal Prod.thy "((a,b): Sigma A B) = (a:A & b:B(a))";