Re: [isabelle] Different behavior in Jedit and Emacs



Just as another data point: I tried the development version with emacs
and it works.

Tobias

Am 20/01/2012 16:09, schrieb Björn Bartels:
> Hi all,
> we just came across  the following problem when using the datatype command. The following datatype definition works when using Jedit but does not work when using Emacs as interface. In the previous distribution the example used to work with Emacs as well.
> 
> theory test
> imports Main
> begin
> 
> datatype 'a tree =
>            leaf "'a"
>          | node "nat \<Rightarrow> 'a tree"        
> 
> datatype 'a dtype  = constr "'a tree"
> 
> end
> 
> 
> When using Emacs, we get the following error message:
> 
> *** Proof failed.
> *** dtype_size fa (constr tree) = 0
> ***  1. Suc 0 = 0
> *** 1 unsolved goal(s)!
> *** The error(s) above occurred for the goal statement:
> *** dtype_size fa (constr tree) = 0
> 
> 
> Thanks for any suggestions!
> 





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