src/Doc/Implementation/Logic.thy
Tue, 30 Jul 2019 20:09:25 +0200 wenzelm clarified global theory context;
Tue, 30 Jul 2019 14:35:29 +0200 wenzelm clarified modules: provide reconstruct_proof / expand_proof at the bottom of proof term construction;
Tue, 23 Jul 2019 19:07:28 +0200 wenzelm discontinued Proofterm.Promise (cf. 725438ceae7c);
Sun, 21 Jul 2019 15:42:43 +0200 wenzelm discontinued ASCII syntax;
Sat, 05 Jan 2019 17:24:33 +0100 wenzelm isabelle update -u control_cartouches;
Thu, 15 Nov 2018 21:33:00 +0100 wenzelm proper citation (amending 98ba42f19995);
Sun, 01 Jul 2018 12:38:37 +0200 wenzelm discontinued pending_shyps: too much complication due to lazy facts;
Fri, 29 Jun 2018 15:54:41 +0200 wenzelm disallow pending hyps;
Wed, 06 Dec 2017 15:46:35 +0100 wenzelm more embedded cartouche arguments;
Sun, 09 Apr 2017 19:03:55 +0200 wenzelm tuned signature -- prefer qualified names;
Fri, 12 Aug 2016 17:53:55 +0200 wenzelm more symbols;
Wed, 13 Apr 2016 18:01:05 +0200 wenzelm eliminated "xname" and variants;
Sat, 09 Apr 2016 13:28:32 +0200 wenzelm clarified context;
Fri, 19 Feb 2016 15:01:38 +0100 wenzelm moved examples to avoid dependency on bulky HOL-Proofs session, e.g. relevant for "isabelle makedist";
Tue, 29 Dec 2015 19:11:23 +0100 wenzelm eliminated obscure macro that is in conflict with amsmath.sty;
Wed, 16 Dec 2015 17:28:49 +0100 wenzelm tuned whitespace;
less more (0) -16 tip