isabelle: src/CTT/bool.thy@6acf3ff0f486 (annotated)

0 a5a9c433f639 Initial revision clasohm parents: diff changeset	1	(* Title: CTT/bool
a5a9c433f639 Initial revision clasohm parents: diff changeset	2	ID: $Id$
a5a9c433f639 Initial revision clasohm parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
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
a5a9c433f639 Initial revision clasohm parents: diff changeset	11	consts Bool :: "t"
a5a9c433f639 Initial revision clasohm parents: diff changeset	12	true,false :: "i"
a5a9c433f639 Initial revision clasohm parents: diff changeset	13	cond :: "[i,i,i]=>i"
a5a9c433f639 Initial revision clasohm parents: diff changeset	14	rules
a5a9c433f639 Initial revision clasohm parents: diff changeset	15	Bool_def "Bool == T+T"
a5a9c433f639 Initial revision clasohm parents: diff changeset	16	true_def "true == inl(tt)"
a5a9c433f639 Initial revision clasohm parents: diff changeset	17	false_def "false == inr(tt)"
a5a9c433f639 Initial revision clasohm parents: diff changeset	18	cond_def "cond(a,b,c) == when(a, %u.b, %u.c)"
a5a9c433f639 Initial revision clasohm parents: diff changeset	19	end

author	nipkow
	Thu, 26 Nov 1998 12:18:08 +0100
changeset 5974	6acf3ff0f486
parent 0	a5a9c433f639
permissions	-rw-r--r--