doc-src/Intro/bool.thy

encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed

Bool = FOL +
types   bool 0
arities bool    :: term
consts tt,ff    :: "bool"
end