doc-src/Intro/bool.thy

moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax

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