Re: [isabelle] Bug in assumption display



On Mon, 19 Jan 2009, Holger Gast wrote:

> I have just upgraded my (Ubuntu) emacs to 22.2.1
> and see the following funny behaviour:
> 
> lemma "[| A; B |] ==> A"
> 
> yields:
> 
> goal (1 subgoal):
>  1. A ==> B ==> A
> 
> with ProofGeneral 3.7.1 (advertised as latest stable),
> while starting the command line "isabelle -I" gives (correctly):
> 
> > lemma "[| A; B |] ==> A";
> proof (prove): step 0
> 
> goal (1 subgoal):
>  1. [| A; B |] ==> A

As far as I know, the situation is still the same as it has been for more 
than 10 years already.  The system allows to write iterated arrows (both
=> on types, and ==> on props, i.e. "types of proofs") in
alternative bracket notation, e.g. like this:

  'a => 'b => 'c	vs.   ['a, 'b] => 'c
  A ==> B ==> C		vs.   [| A; B |] ==> C

Printing is controlled by print modes, with positive and negative modes to 
allow explicit control independent of defaults coming from somewhere:

  no_type_brackets	      type_brackets
  no_brackets		      brackets

The default of the Isabelle distribution is no_type_brackets and brackets.  
(Personally I always use no_type_brackets and no_brackets, both for 
uniformity and for improved readability of nested rules; it also requires 
less explanations to new users, assuming that "currying" is known 
already.)


	Makarius





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