Re: [isabelle] can anyone explain this?



On Tue, 27 Mar 2007, Stefan Berghofer wrote:

> Jeremy Dawson wrote:
> > *** Unknown theorem(s) "bin_nth_0"
> > *** At command "lemmas" (line 40 of
> > "/home/users/jeremy/isabelle/l4/bg.thy").
> > 
> > [...]
> > 
> > Does anyone know why this might be?
> 
>
> and then add the corresponding legacy ML bindings later by
> 
>   ML {*
>   val bin_nth_0 = thm "bin_nth_0";
>   val bin_nth_Suc = thm "bin_nth_Suc";
>   *}

A general note to anybody working with recent development snapshots: with 
the advent of ML antiquotations, the need for various legacy ML bindings 
has disappeared altogether.  See the NEWS file within the sources for 
typical examples.  This works uniformly for any kind of ML text 
incorporated into an Isar theory.  For example:

  apply (tactic "ALLGOALS (force_tac @{clasimpset}")

No need to worry about changing dynamic contexts etc.  Everything is 
statically scoped (at compile-time) as expected.


	Makarius





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