(*
$Id: ex.thy,v 1.2 2004/11/23 15:14:34 webertj Exp $
Author: Martin Strecker
*)
header {* Elimination of Connectives *}
(*<*) theory ex imports Main begin (*>*)
text {* In classical propositional logic, the connectives @{text "=, \,
\"} can be replaced by @{text "\, \, False"}. Define
corresponding simplification rules as lemmas and prove their correctness. (You
may use automated proof tactics.) *}
text {* What is the result of your translation for the formula @{text "A \
(B \ C) = A"}? (You can use Isabelle's simplifier to compute the result
by using the simplifier's @{text "only"} option.) *}
(*<*) end (*>*)