# HG changeset patch
# User berghofe
# Date 909175035 -7200
# Node ID 149d435aa4d71addb85ecdd5722011f168a91dc3
# Parent  a396eff81fdaab0cea34140860a1ff594ed06d69
Added theorem bool_induct (for rep_datatype).

diff -r a396eff81fda -r 149d435aa4d7 src/HOL/equalities.ML
--- 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);