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.

Larry Paulson


> 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
>      message:
>      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 MHonArc.