wenzelm [Sat, 12 Jun 2021 18:22:07 +0200] rev 60298
use more antiquotations;
wenzelm [Sat, 12 Jun 2021 18:06:27 +0200] rev 60297
use more antiquotations;
wenzelm [Sat, 12 Jun 2021 14:29:10 +0200] rev 60296
ML antiquotations for Rule.Thm, with special treatment of symmetric rule;
wenzelm [Sat, 12 Jun 2021 14:27:03 +0200] rev 60295
updated TODO;
wenzelm [Fri, 11 Jun 2021 11:49:34 +0200] rev 60294
ML antiquotation for formally checked Rule.Eval;
wenzelm [Thu, 10 Jun 2021 17:06:32 +0200] rev 60293
tuned signatures (SML'97 allows type abbreviations);
tuned comments;
wenzelm [Thu, 10 Jun 2021 12:53:02 +0200] rev 60292
more TODO;
wenzelm [Thu, 10 Jun 2021 12:48:50 +0200] rev 60291
clarified theory context: avoid global "val thy = ..." hanging around (left-over from Isabelle2005), which is apt to various pitfalls;
wenzelm [Thu, 10 Jun 2021 12:23:57 +0200] rev 60290
clarified theory context: from current command instead of earlier state;
wenzelm [Thu, 10 Jun 2021 11:54:20 +0200] rev 60289
clarified command name: this is to register already defined rule sets in the Knowledge Store;