Thu, 11 Dec 2008 20:31:45 +0100 unified ids for ancestors and checkpoints, removed obsolete history of checkpoints;
wenzelm [Thu, 11 Dec 2008 20:31:45 +0100] rev 29069
unified ids for ancestors and checkpoints, removed obsolete history of checkpoints; tuned representation of internal node names -- avoid string copies; tuned signature;
Thu, 11 Dec 2008 20:17:57 +0100 removed spurious exception_trace;
wenzelm [Thu, 11 Dec 2008 20:17:57 +0100] rev 29068
removed spurious exception_trace;
Thu, 11 Dec 2008 17:32:37 +0100 print_theorems: more robust difference, even after finished proof;
wenzelm [Thu, 11 Dec 2008 17:32:37 +0100] rev 29067
print_theorems: more robust difference, even after finished proof;
Thu, 11 Dec 2008 17:31:23 +0100 export context_node;
wenzelm [Thu, 11 Dec 2008 17:31:23 +0100] rev 29066
export context_node;
Thu, 11 Dec 2008 17:04:46 +0100 merged
wenzelm [Thu, 11 Dec 2008 17:04:46 +0100] rev 29065
merged
Wed, 10 Dec 2008 22:55:15 +0100 more antiquotations;
wenzelm [Wed, 10 Dec 2008 22:55:15 +0100] rev 29064
more antiquotations;
Thu, 11 Dec 2008 16:50:18 +0100 pcpodef package: state two goals, instead of encoded conjunction;
wenzelm [Thu, 11 Dec 2008 16:50:18 +0100] rev 29063
pcpodef package: state two goals, instead of encoded conjunction;
Thu, 11 Dec 2008 16:30:35 +0100 recovered goal_pat;
wenzelm [Thu, 11 Dec 2008 16:30:35 +0100] rev 29062
recovered goal_pat;
Thu, 11 Dec 2008 16:09:12 +0100 inhabitance goal is now stated in original form and result contracted --
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.;
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;
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip