| Thu, 23 Jun 2016 11:01:14 +0200 | wenzelm | tuned signature; | file | diff | annotate |
| Sat, 15 Aug 2015 20:07:05 +0200 | wenzelm | clarified context; | file | diff | annotate |
| Mon, 27 Jul 2015 23:40:39 +0200 | wenzelm | tuned signature; | file | diff | annotate |
| Thu, 09 Jul 2015 22:36:31 +0200 | wenzelm | SUBPROOF and Subgoal.FOCUS combinators use anonymous quasi-bound variables (like the Simplifier); | file | diff | annotate |
| Wed, 08 Jul 2015 19:28:43 +0200 | wenzelm | Variable.focus etc.: optional bindings provided by user; | file | diff | annotate |
| 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); | file | diff | annotate |
| Thu, 02 Jul 2015 12:39:08 +0200 | wenzelm | clarified module; | file | diff | annotate | base |