src/CTT/Bool.thy
author wenzelm
Fri Sep 16 23:01:29 2005 +0200 (2005-09-16)
changeset 17441 5b5feca0344a
parent 3837 d7f033c74b38
child 19761 5cd82054c2c6
permissions -rw-r--r--
converted to Isar theory format;
     1 (*  Title:      CTT/bool
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1991  University of Cambridge
     5 *)
     6 
     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
    13 
    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 
    27 end