|
1474
|
1 |
(* Title: CTT/bool
|
|
0
|
2 |
ID: $Id$
|
|
1474
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
0
|
4 |
Copyright 1991 University of Cambridge
|
|
|
5 |
*)
|
|
|
6 |
|
|
17441
|
7 |
header {* The two-element type (booleans and conditionals) *}
|
|
|
8 |
|
|
|
9 |
theory Bool
|
|
|
10 |
imports CTT
|
|
|
11 |
uses "~~/src/Provers/typedsimp.ML" "rew.ML"
|
|
|
12 |
begin
|
|
0
|
13 |
|
|
17441
|
14 |
consts
|
|
|
15 |
Bool :: "t"
|
|
|
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 |
|
|
0
|
27 |
end
|