* Isar/Pure: emulation of instantiation tactics (rule_tac, cut_tac,
etc.) now consider the syntactic context of assumptions, giving a
better chance to get type-inference of the arguments right (this is
especially important for locales);
* system: refrain from any attempt at filtering input streams; no
longer support ``8bit'' encoding of old isabelle font, instead proper
iso-latin characters may now be used;
(* Title: ZF/bool.thy
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
Booleans in Zermelo-Fraenkel Set Theory
2 is equal to bool, but serves a different purpose
*)
Bool = pair +
consts
bool :: i
cond :: [i,i,i]=>i
not :: i=>i
"and" :: [i,i]=>i (infixl 70)
or :: [i,i]=>i (infixl 65)
xor :: [i,i]=>i (infixl 65)
syntax
"1" :: i ("1")
"2" :: i ("2")
translations
"1" == "succ(0)"
"2" == "succ(1)"
defs
bool_def "bool == {0,1}"
cond_def "cond(b,c,d) == if(b=1,c,d)"
not_def "not(b) == cond(b,0,1)"
and_def "a and b == cond(a,b,0)"
or_def "a or b == cond(a,1,b)"
xor_def "a xor b == cond(a,not(b),b)"
end