equal
deleted
inserted
replaced
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 |
9 open Bool; |
9 open Bool; |
10 |
10 |
11 val bool_defs = [bool_def,one_def,cond_def]; |
11 val bool_defs = [bool_def,cond_def]; |
12 |
12 |
13 (* Introduction rules *) |
13 (* Introduction rules *) |
14 |
14 |
15 goalw Bool.thy bool_defs "1 : bool"; |
15 goalw Bool.thy bool_defs "1 : bool"; |
16 by (rtac (consI1 RS consI2) 1); |
16 by (rtac (consI1 RS consI2) 1); |