equal
deleted
inserted
replaced
9 theory Bool |
9 theory Bool |
10 imports CTT |
10 imports CTT |
11 begin |
11 begin |
12 |
12 |
13 definition |
13 definition |
14 Bool :: "t" |
14 Bool :: "t" where |
15 "Bool == T+T" |
15 "Bool == T+T" |
16 |
16 |
17 true :: "i" |
17 definition |
|
18 true :: "i" where |
18 "true == inl(tt)" |
19 "true == inl(tt)" |
19 |
20 |
20 false :: "i" |
21 definition |
|
22 false :: "i" where |
21 "false == inr(tt)" |
23 "false == inr(tt)" |
22 |
24 |
23 cond :: "[i,i,i]=>i" |
25 definition |
|
26 cond :: "[i,i,i]=>i" where |
24 "cond(a,b,c) == when(a, %u. b, %u. c)" |
27 "cond(a,b,c) == when(a, %u. b, %u. c)" |
25 |
28 |
26 lemmas bool_defs = Bool_def true_def false_def cond_def |
29 lemmas bool_defs = Bool_def true_def false_def cond_def |
27 |
30 |
28 |
31 |