Re: [isabelle] PIDE Display of Assumptions



On Friday, June 29, 2012 at 16:27:56 (+0100), Makarius wrote:
 > 
 > > At the moment, however, the curried notation of the meta implication drives me crazy :-)
 > > My current subgoal structurally looks like this:
 > >
 > >    (A ⟹ B ⟹ C) ⟹ (D ⟹ F) ⟹ G ⟹ H ⟹ I ⟹ J
 > >
 > > and I'd rather have it like this again:
 > >
 > >    [[A; B] ⟹ C; D ⟹ F; G; H; I] ⟹ J
 > >
 > > Is there a display option for this?
 > 
 > This is called "print mode" in Isabelle terminology.  E.g.
 > 
 >    isabelle jedit -m brackets
 > 
 > will recover the above special Isabelle syntax for nested implications.

Is there a way to make that printmode the default 
in ones etc/settings, for example? I have to admit 
I am very fond of this special syntax too and have no
problem with interpreting them in my head as

 [A,B]     [D]
   C        F    G   H   I 
  ------------------------
              J

which is the style that usually appears in textbooks on 
natural deduction. For example, the Gentzen book would 
write the impI- and  orE-rules as

       [A]
        B
     -------
     A --> B


           [A] [B]
  A v B     C   C
  ---------------
        C

which is not very different from Larry's bracket notation.


My 2 cents,
Christian





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.