doc-src/Intro/bool.thy
author bulwahn
Fri, 03 Dec 2010 08:40:47 +0100
changeset 40921 a516fbdd9931
parent 32960 69916a850301
permissions -rw-r--r--
improving sledgehammer_tactic and adding relevance filtering to the tactic

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