# HG changeset patch
# User berghofe
# Date 909175009 -7200
# Node ID a396eff81fdaab0cea34140860a1ff594ed06d69
# Parent  7e2cf2820684683eef4b906e70b7b44c9848e6e8
Added theorem unit_induct (for rep_datatype).

diff -r 7e2cf2820684 -r a396eff81fda src/HOL/Prod.ML
--- 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";