src/HOL/ex/cla.ML

 by (Blast_tac 1);
 result();
 
 (*From Davis, Obvious Logical Inferences, IJCAI-81, 530-531
   Fast_tac indeed copes!*)
-goal Prod.thy "(ALL x. F(x) & ~G(x) --> (EX y. H(x,y) & J(y))) & \
+goal Product_Type.thy "(ALL x. F(x) & ~G(x) --> (EX y. H(x,y) & J(y))) & \
 \             (EX x. K(x) & F(x) & (ALL y. H(x,y) --> K(y))) &   \
 \             (ALL x. K(x) --> ~G(x))  -->  (EX x. K(x) & J(x))";
 by (Fast_tac 1);
 result();
 
 (*From Rudnicki, Obvious Inferences, JAR 3 (1987), 383-393.  
   It does seem obvious!*)
-goal Prod.thy
+goal Product_Type.thy
     "(ALL x. F(x) & ~G(x) --> (EX y. H(x,y) & J(y))) &        \
 \    (EX x. K(x) & F(x) & (ALL y. H(x,y) --> K(y)))  &        \
 \    (ALL x. K(x) --> ~G(x))   -->   (EX x. K(x) --> ~G(x))";
 by (Fast_tac 1);
 result();

 \     (ALL x. ~healthy(x) & cyclist(x) --> ~honest(x))  \
 \     --> (ALL x. grocer(x) --> ~cyclist(x))";
 by (Blast_tac 1);
 result();
 
-goal Prod.thy
+goal Product_Type.thy
     "(ALL x y. R(x,y) | R(y,x)) &                \
 \    (ALL x y. S(x,y) & S(y,x) --> x=y) &        \
 \    (ALL x y. R(x,y) --> S(x,y))    -->   (ALL x y. S(x,y) --> R(x,y))";
 by (Blast_tac 1);
 result();