author | berghofe |
Fri, 23 Oct 1998 22:37:15 +0200 | |
changeset 5762 | 149d435aa4d7 |
parent 5761 | a396eff81fda |
child 5763 | 58ed0a78906d |
--- 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);