SubAndCondContextScript.sml

1Theory SubAndCondContext[bare]
2Libs
3  HolKernel Parse boolLib
4
5(* ------------------------------------------------------------------------- *)
6(* CASES_ELIM: pull a boolean under a predicate through cases on that        *)
7(* boolean.  Sub_and_cond.sml formerly proved this as it loaded.             *)
8(* ------------------------------------------------------------------------- *)
9
10Theorem CASES_ELIM:
11  !P p. P p <=> (p ==> P T) /\ (~p ==> P F)
12Proof
13  REPEAT GEN_TAC THEN ASM_CASES_TAC ``p:bool`` THEN ASM_REWRITE_TAC []
14QED