[isabelle-dev] unfold_set_consts

Jasmin Christian Blanchette jasmin.blanchette at gmail.com
Wed Dec 28 17:31:32 CET 2011


Am 28.12.2011 um 15:15 schrieb Makarius:

> Due to the re-introduction of 'a set as proper type constructor, change 4c629115e3ab in src/HOL/Tools/Meson/meson.ML makes unfold_set_const_simps vacuous.
> 
> A brief inspection suggests that the corresponding "unfold_set_consts" configuration option is now also obsolete.

Yes, those are things I will clean up once I'm back in January. Cf. my 18 August emails on the list.

Jasmin




More information about the isabelle-dev mailing list