equal
deleted
inserted
replaced
1 (* Title: CTT/bool |
1 (* Title: CTT/bool |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1991 University of Cambridge |
4 Copyright 1991 University of Cambridge |
5 |
|
6 The two-element type (booleans and conditionals) |
|
7 *) |
5 *) |
8 |
6 |
9 Bool = CTT + |
7 header {* The two-element type (booleans and conditionals) *} |
10 |
8 |
11 consts Bool :: "t" |
9 theory Bool |
12 true,false :: "i" |
10 imports CTT |
13 cond :: "[i,i,i]=>i" |
11 uses "~~/src/Provers/typedsimp.ML" "rew.ML" |
14 rules |
12 begin |
15 Bool_def "Bool == T+T" |
13 |
16 true_def "true == inl(tt)" |
14 consts |
17 false_def "false == inr(tt)" |
15 Bool :: "t" |
18 cond_def "cond(a,b,c) == when(a, %u. b, %u. c)" |
16 true :: "i" |
|
17 false :: "i" |
|
18 cond :: "[i,i,i]=>i" |
|
19 defs |
|
20 Bool_def: "Bool == T+T" |
|
21 true_def: "true == inl(tt)" |
|
22 false_def: "false == inr(tt)" |
|
23 cond_def: "cond(a,b,c) == when(a, %u. b, %u. c)" |
|
24 |
|
25 ML {* use_legacy_bindings (the_context ()) *} |
|
26 |
19 end |
27 end |