isabelle: src/CTT/Bool.thy@27e6d344d724 (annotated)

1474 3f7d67927fe2 expanded tabs clasohm parents: 0 diff changeset	1	(* Title: CTT/bool
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	2	ID: $Id$
1474 3f7d67927fe2 expanded tabs clasohm parents: 0 diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	4	Copyright 1991 University of Cambridge
a5a9c433f639 Initial revision clasohm parents: diff changeset	5
a5a9c433f639 Initial revision clasohm parents: diff changeset	6	The two-element type (booleans and conditionals)
a5a9c433f639 Initial revision clasohm parents: diff changeset	7	*)
a5a9c433f639 Initial revision clasohm parents: diff changeset	8
a5a9c433f639 Initial revision clasohm parents: diff changeset	9	Bool = CTT +
a5a9c433f639 Initial revision clasohm parents: diff changeset	10
1474 3f7d67927fe2 expanded tabs clasohm parents: 0 diff changeset	11	consts Bool :: "t"
3f7d67927fe2 expanded tabs clasohm parents: 0 diff changeset	12	true,false :: "i"
3f7d67927fe2 expanded tabs clasohm parents: 0 diff changeset	13	cond :: "[i,i,i]=>i"
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	14	rules
1474 3f7d67927fe2 expanded tabs clasohm parents: 0 diff changeset	15	Bool_def "Bool == T+T"
3f7d67927fe2 expanded tabs clasohm parents: 0 diff changeset	16	true_def "true == inl(tt)"
3f7d67927fe2 expanded tabs clasohm parents: 0 diff changeset	17	false_def "false == inr(tt)"
3837 d7f033c74b38 fixed dots; wenzelm parents: 1474 diff changeset	18	cond_def "cond(a,b,c) == when(a, %u. b, %u. c)"
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	19	end

author	berghofe
	Wed, 20 Feb 2002 15:58:38 +0100
changeset 12907	27e6d344d724
parent 3837	d7f033c74b38
child 17441	5b5feca0344a
permissions	-rw-r--r--