isabelle: Changelog

Mercurial Mercurial > repos > isabelle / changelog

Thu, 11 Dec 2008 16:09:12 +0100 inhabitance goal is now stated in original form and result contracted --

changeset

wenzelm [Thu, 11 Dec 2008 16:09:12 +0100] rev 29061

inhabitance goal is now stated in original form and result contracted -- the previous attempt with contracted goal and initial unfolding did not work, because it disrupted the Isar proof structure (e.g. ?thesis);

Thu, 11 Dec 2008 12:02:48 +0100 tuned signature: pcpodef_proof, pcpodef_proof_cmd etc.;

changeset

wenzelm [Thu, 11 Dec 2008 12:02:48 +0100] rev 29060

tuned signature: pcpodef_proof, pcpodef_proof_cmd etc.; more antiquotations; explicit Theory.requires; adapted to recent changes in ~~/src/HOL/Tools/typedef_package.ML; misc tuning and simplification;

Thu, 11 Dec 2008 11:55:46 +0100 add_typedef: unfold set_def in tactical proof as well;

changeset

wenzelm [Thu, 11 Dec 2008 11:55:46 +0100] rev 29059

add_typedef: unfold set_def in tactical proof as well;

Thu, 11 Dec 2008 10:41:53 +0100 merged

changeset

wenzelm [Thu, 11 Dec 2008 10:41:53 +0100] rev 29058

merged

Thu, 11 Dec 2008 10:41:37 +0100 Theory.checkpoint before commencing proof;

changeset

wenzelm [Thu, 11 Dec 2008 10:41:37 +0100] rev 29057

Theory.checkpoint before commencing proof;