Added theorem unit_induct (for rep_datatype).

--- a/src/HOL/Prod.ML	Fri Oct 23 22:36:15 1998 +0200
+++ b/src/HOL/Prod.ML	Fri Oct 23 22:36:49 1998 +0200
@@ -432,6 +432,11 @@
 Addsimprocs [unit_eq_proc];
 
 
+Goal "P () ==> P x";
+by (Simp_tac 1);
+qed "unit_induct";
+
+
 (*This rewrite counters the effect of unit_eq_proc on (%u::unit. f u),
   replacing it by f rather than by %u.f(). *)
 Goal "(%u::unit. f()) = f";