[isabelle-dev] Isabelle/HOL axiom "iff" is redundant

[Alexander Krauss]

> Has anyone else noticed that axiom "True_or_False" implies axiom
> "iff"? (You can just do a proof by cases on P and Q.)

Here the case seems a little different, as eq_reflection is probably not 
involved (or is it?). So maybe this is really redundant, but I am not sure.

> I'm guessing that the origins of this redundancy are historical---I
> suppose that True_or_False was probably introduced later in the
> development so that intuitionistic lemmas could be kept separate from
> the classical ones.

This seems like a sensible explanation... Was there ever a non-classical 
HOL? At least in the "known history" the axioms were always sitting 
there, side by side:

http://isabelle.in.tum.de/repos/Old_HOL/annotate/7949f97df77a/hol.thy#l105

Alex