[isabelle-dev] Towards the next release

[Lawrence Paulson]

There is something I'd like to mention, not a big deal, but worth considering.

I've been doing some proofs lately after a long gap, making myself a combination of a novice and expert. And I've got confused by things that would probably confuse true novices even more.

Here are two instantiations, both of which simply do overloading but justify no properties. Such instantiations always succeed, because there is nothing to prove. But I discovered that you have to be very careful to introduce overloading correctly. If it's wrong, the instantiation effectively does nothing; when that happens, a warning ought to appear.

The overloading rules are quite tricky. I don't understand why the first instantiation requires a definition of sup_hf (including the type in the constant name), while the second one simply requires a definition of minus. Perhaps because there is an explicit type in the first instantiation and not on the second one? In any event, if the user gets wrong, a warning would be appropriate. And I hope that wouldn't be difficult to implement.

instantiation hf :: sup
begin

definition sup_hf :: "hf \<Rightarrow> hf \<Rightarrow> hf"
  where "sup_hf a b = ..."

instantiation hf :: minus
begin
definition minus_hf where
  "minus A B = ...
instance proof 


Larry

On 12 Apr 2012, at 10:02, Makarius wrote:

> Dear all,
> 
> we need to get to a more concrete release schedule.  Presently I would like to aim for late May, which means we need to start consolidating and converging about now.
> 
> Are there any further big things in the pipeline?
> 
> This is also a good point to populate NEWS, CONTRIBUTORS, and update manuals to cover new things.  (I am speaking to myself here as well.)
> 
> 
> 	Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev