Thanks, Konrad! I see that the HOL light BOOL_CASES_AX is proved in class.ml using the result I mentioned, EXCLUDED_MIDDLE, which class.ml says is derived from Beeson's book:
let BOOL_CASES_AX = prove (`!t. (t <=> T) \/ (t <=> F)`, GEN_TAC THEN DISJ_CASES_TAC(SPEC `t:bool` EXCLUDED_MIDDLE) THEN ASM_REWRITE_TAC[]);; -- Best, Bill ------------------------------------------------------------------------------ Learn Graph Databases - Download FREE O'Reilly Book "Graph Databases" is the definitive new guide to graph databases and their applications. Written by three acclaimed leaders in the field, this first edition is now available. Download your free book today! http://p.sf.net/sfu/13534_NeoTech _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
