Added theorem bool_induct (for rep_datatype).

--- a/src/HOL/equalities.ML	Fri Oct 23 22:36:49 1998 +0200
+++ b/src/HOL/equalities.ML	Fri Oct 23 22:37:15 1998 +0200
@@ -720,6 +720,8 @@
 by Auto_tac;
 qed "all_bool_eq";
 
+bind_thm ("bool_induct", conjI RS (all_bool_eq RS iffD2) RS spec);
+
 Goal "(EX b::bool. P b) = (P True | P False)";
 by Auto_tac;
 by (case_tac "b" 1);