changeset 1461 | 6bcb44e4d6e5 |
parent 760 | f0200e91b272 |
child 2469 | b50b8c0eec01 |
1460:5a6f2aabd538 | 1461:6bcb44e4d6e5 |
---|---|
1 (* Title: ZF/bool |
1 (* Title: ZF/bool |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Martin D Coen, Cambridge University Computer Laboratory |
3 Author: Martin D Coen, Cambridge University Computer Laboratory |
4 Copyright 1992 University of Cambridge |
4 Copyright 1992 University of Cambridge |
5 |
5 |
6 For ZF/bool.thy. Booleans in Zermelo-Fraenkel Set Theory |
6 For ZF/bool.thy. Booleans in Zermelo-Fraenkel Set Theory |
7 *) |
7 *) |
8 |
8 |
87 qed_goalw "xor_type" Bool.thy [xor_def] |
87 qed_goalw "xor_type" Bool.thy [xor_def] |
88 "[| a:bool; b:bool |] ==> a xor b : bool" |
88 "[| a:bool; b:bool |] ==> a xor b : bool" |
89 (fn prems=> [ (typechk_tac(prems@[bool_1I, bool_0I, cond_type, not_type])) ]); |
89 (fn prems=> [ (typechk_tac(prems@[bool_1I, bool_0I, cond_type, not_type])) ]); |
90 |
90 |
91 val bool_typechecks = [bool_1I, bool_0I, cond_type, not_type, and_type, |
91 val bool_typechecks = [bool_1I, bool_0I, cond_type, not_type, and_type, |
92 or_type, xor_type] |
92 or_type, xor_type] |
93 |
93 |
94 val bool_simps = [cond_1,cond_0,not_1,not_0,and_1,and_0,or_1,or_0,xor_1,xor_0]; |
94 val bool_simps = [cond_1,cond_0,not_1,not_0,and_1,and_0,or_1,or_0,xor_1,xor_0]; |
95 |
95 |
96 val bool_ss0 = ZF_ss addsimps bool_simps; |
96 val bool_ss0 = ZF_ss addsimps bool_simps; |
97 |
97 |