Re: [isabelle] Experimental tweaks to make HOL intuitionistic-by-default
The problem with elim declarations is that your rules (once exported from the locale) no longer have the necessary elim-form. You could declare them as such WITHIN the locale. They won’t work as you wish outside.
So overall, I don’t think you can build all of HOL while separating out the classical part. It is just too huge, and there are too many things to change.
> On 21 Nov 2014, at 22:09, Josh Tilles <merelyapseudonym at gmail.com> wrote:
> - The problem is that the elim rules break:
> - on the line "declare NonIntuitionistic.iffCE [elim!]" we see the
> exception THM 1 raised (line 332 of "drule.ML"):
> RSN: no unifiers
> PROP NonIntuitionistic ⟹ ?P = ?Q ⟹ (?P ⟹ ?Q ⟹ ?R) ⟹ (¬ ?P ⟹ ¬ ?Q ⟹
> ?R) ⟹ ?R
> PROP NonIntuitionistic ⟹ (¬ ?P ⟹ ?P) ⟹ ?P
This archive was generated by a fusion of
Pipermail (Mailman edition) and