author | nipkow |
Thu, 11 Jul 2002 10:48:30 +0200 | |
changeset 13347 | 867f876589e7 |
parent 3837 | d7f033c74b38 |
child 17441 | 5b5feca0344a |
permissions | -rw-r--r-- |
(* Title: CTT/bool ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1991 University of Cambridge The two-element type (booleans and conditionals) *) Bool = CTT + consts Bool :: "t" true,false :: "i" cond :: "[i,i,i]=>i" rules Bool_def "Bool == T+T" true_def "true == inl(tt)" false_def "false == inr(tt)" cond_def "cond(a,b,c) == when(a, %u. b, %u. c)" end