src/Doc/Implementation/Logic.thy
Sun, 05 Jul 2015 15:02:30 +0200 wenzelm simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
Wed, 01 Apr 2015 22:40:07 +0200 wenzelm misc tuning -- keep name space more clean;
Fri, 06 Mar 2015 15:58:56 +0100 wenzelm Thm.cterm_of and Thm.ctyp_of operate on local context;
Mon, 20 Oct 2014 23:17:28 +0200 wenzelm tuned spacing;
Tue, 07 Oct 2014 21:29:59 +0200 wenzelm more cartouches;
Sun, 05 Oct 2014 22:47:07 +0200 wenzelm prefer @{cite} antiquotation;
less more (0) -6 tip